talk – Chalmers Security Seminar
High-assurance cryptography leverages methods from program verification and cryptography engineering to deliver efficient cryptographic software with machine-checked proofs of memory safety, functional correctness, provable security, and absence of timing leaks. Traditionally, these guarantees are established under a sequential execution semantics. However, this semantics is not aligned with the behavior of modern processors that make use of speculative execution to improve performance. This mismatch, combined with the high-profile Spectre-style attacks that exploit speculative execution, naturally casts doubts on the robustness of high-assurance cryptography guarantees. In this paper, we dispel these doubts by showing that the benefits of high-assurance cryptography extend to speculative execution, costing only a modest performance overhead. We build atop the Jasmin verification framework an end-to-end approach for proving properties of cryptographic software under speculative execution, and validate our approach experimentally with efficient, functionally correct assembly implementations of ChaCha20 and Poly1305, which are secure against both traditional timing and speculative execution attacks.
Read More ›talk – Chalmers Security Seminar
There is a long line of research on how to control information flow in pure programming languages. In Haskell, for instance, the MAC library [Russo 2015] provides IFC primitives that allows programmers to write (statically) secure programs. MAC enforces security by controlling the interaction of an indexed monad for print effects, MAC, and a type for labeling data, Labeled. In this talk, I will present a different point in the design space of IFC libraries which in some sense refines MAC. The starting point will be a pure language where the monad for print effects—think of IO in Haskell restricted to print—keeps track of the output channels within the type. Looking at MAC in this setting, we see that one can safely embed effectful computations into the MAC monad. It appears that in this extended setting the MAC monad is redundant in the sense that we can express its interface in terms of indexed IO and Labeled. Arguably, this refinement yields a library which is: conceptually cleaner; more compositional; and it allows more programs to typecheck. This talk is based on a paper that Alejandro Russo and I are currently preparing for submission.
Read More ›talk – Chalmers Security Seminar
This presentation provides an introduction to fuzz testing of automotive systems with a focus on both process and practical topics. We first discuss the typical automotive development process to better understand where the fuzz testing activity fits into the overall process. We also discuss common practical pitfalls and challenges when performing fuzz testing of automotive systems. Based on this understanding, a few examples of how fuzz testing can be performed in practice, including how to build a fuzz testing environment for automotive systems, are explained. Last, we also explore how to perform continuous fuzz testing using automated tools and virtual ECUs as part of a CI/CD pipeline.
Read More ›talk – Chalmers Security Seminar
In this talk, I will present some work in progress on using IFC principles for enforcing GDPR-style privacy principles. Privacy legislation such as the GDPR specifies legal requirements for protecting the private data of individuals but remains vague about how to implement such requirements in practice. Traditional security mechanisms such as cryptography or access control are blunt instruments for this job since they typically cannot distinguish between intended and inappropriate usage of private data. To complement them, I propose a programming language-based framework that uses IFC mechanisms to enforce privacy principles such as purpose limitation and data minimization. I will start by illustrating how these principles are ultimately about information flow and how they can be integrated in existing IFC frameworks. I’ll then sketch a simple type system for tracking secure and private information flow.
Read More ›talk – Chalmers Security Seminar
Information flow properties are the semantic cornerstone of a wide range of program transformations, program analyses, and security properties. The variety of information that can be transmitted from inputs to outputs in a deterministic system can be elegantly and very generally captured by representing information as equivalence relations over the sets of possible values, using an equivalence relation on the input domain to model what may be learned, and an equivalence relation on the output to model what may be observed. The set of equivalence relations over a given set of values form a lattice, where the partial order models containment of information, and lattice join models the effect of combining information. This elegant and general structure is sometimes referred to as the lattice of information (Landauer & Redmond CSFW'93). In this work we identify an abstraction of information flow which has not been studied previously, namely disjunctive dependency. We argue that this is both interesting in its own right, providing for example an information flow based semantic model of Chinese-wall policies, and potentially provides increased precision in the application of dependency analysis to computation of quantitative properties. We achieve this via a generalization of the lattice of information to a quantale, a lattice equipped with a tensor operation where the lattice join corresponds to the disjunctive combination of information, and tensor corresponds to conjunctive combination.
Read More ›