PLAS’19- Proceedings of the 14th ACM SIGSAC Workshop on Programming Languages and Analysis for SecurityFull Citation in the ACM Digital Library
SESSION: Session 1: Malware and Cryptography
Are All Firewall Systems Equally Powerful?
Firewalls are a fundamental tool for managing and protecting computer networks. They not only permit specifying which packets are allowed to enter a network, but also how these packets are modified by translating IP addresses and performing port redirection (NAT). Many firewalls systems are available which provide different tools and configuration languages. In contrast with the intuition, the most widespread languages cannot express the same configurations, even when simple filtering and NAT transformations are considered. This paper formally investigates the power of firewall languages of the most used tools in Unix and Linux. In particular, we introduce two kinds of expressivity. The first concerns the ways a packet can be transformed by NAT. According to this criterion iptables is strictly more expressive than ipfw and pf that are equivalent. The second kind is more finer-grained and considers the dependencies among the management of all packets. Our results show that some configurations are expressible in a system, but not in another one. Indeed, iptables is incomparable with the others, and ipfw is more expressive than pf.
Unacceptable Behavior: Robust PDF Malware Detection Using Abstract Interpretation
State-of-the-art approaches use machine learning to learn features that characterize PDF malware, which makes them subject to adversarial attacks that mimic the structure of benign documents. In this paper, we instead propose to detect malicious code inside a PDF by statically reasoning about its possible behavior using abstract interpretation. A comparison with state-of-the-art PDF malware detection tools shows that our conservative abstract interpretation approach achieves similar accuracy, is more resilient to evasion attacks, and provides interpretable reports.
High-Level Cryptographic Abstractions
The interfaces exposed by commonly used cryptographic libraries are clumsy, complicated, and assume an understanding of cryptographic algorithms. The challenge is to design high-level abstractions that require minimum knowledge and effort to use while also allowing maximum control when needed.
This paper proposes such high-level abstractions consisting of simple cryptographic primitives and full declarative configuration. These abstractions can be implemented on top of any cryptographic library in any language. We have implemented these abstractions in Python, and used them to write a wide variety of well-known security protocols, including Signal, Kerberos, and TLS.
We show that programs using our abstractions are much smaller and easier to write than using low-level libraries, where size of security protocols implemented is reduced by about a third on average. We show our implementation incurs a small overhead, less than 5 microseconds for shared key operations and less than 341 microseconds (< 1%) for public key operations. We also show our abstractions are safe against main types of cryptographic misuse reported in the literature.
SESSION: Session 2: Information Flow
Simple Noninterference by Normalization
Information-flow control (IFC) languages ensure programs preserve the confidentiality of sensitive data. Noninterference, the desired security property of such languages, states that public outputs of programs must not depend on sensitive inputs. In this paper, we show that noninterference can be proved using normalization. Unlike arbitrary terms, normal forms of programs are well-principled and obey useful syntactic properties-hence enabling a simpler proof of noninterference. Since our proof is syntax-directed, it offers an appealing alternative to traditional semantic based techniques to prove noninterference.
In particular, we prove noninterference for a static IFC calculus, based on Haskell’s seclib library, using normalization. Our proof follows by straightforward induction on the structure of normal forms. We implement normalization using normalization by evaluation and prove that the generated normal forms preserve semantics. Our results have been verified in the Agda proof assistant.