The ongoing renaissance in artificial intelligence (AI) has led to the advent of data-driven machine learning (ML) methods deployed within components for sensing, actuation, and control in safety-critical cyber-physical systems (CPS). While such learning-enabled components (LECs) are enabling autonomy in systems like autonomous vehicles and robots, ensuring such components operate reliably in all scenarios is extraordinarily challenging, as demonstrated in part through recent accidents in semi-autonomous/autonomous CPS and by adversarial ML attacks. We will discuss formal methods for assuring specifications---mostly robustness and safety---in autonomous CPS and subcomponents thereof using our software tools NNV and Veritex, developed as part of an ongoing DARPA Assured Autonomy project. These tools have been evaluated in CPS development with multiple industry partners in automotive, aerospace, and robotics domains, and allow for formally analyzing neural networks and their usage in closed-loop systems. We will also discuss relevant ongoing community activities we help organize, such as the Verification of Neural Networks Competition (VNN-COMP) held with the International Conference on Computer-Aided Verification (CAV) the past few years, as well as the AI and Neural Network Control Systems (AINNCS) category of the hybrid systems verification competition (ARCH-COMP) also held the past few years. We will conclude with a discussion of future directions in the broader safe and trustworthy AI domain, such as in new projects verifying neural networks used in medical imaging analysis.

A counterfactual explanation refers to the problem of finding a minimum change to a given input instance that will result in a desired prediction under a given, trained machine learning model. This is useful to extract actionable knowledge such as "reducing your weight by 10 kg will reduce your risk of stroke by 80%" (regression) or "you will be eligible for the loan if you increase your annual salary by $10k" (classification). Counterfactual explanations are closely related to adversarial examples, where one seeks to trick a model into misclassifying a given instance; and to model verification, where one seeks to prove (or find a counterexample to) a given property of a model. A counterfactual explanation can be formulated as an optimization problem of minimizing the change (in some distance) to the input instance subject to the model producing the desired prediction. Here we focus on classification and regression models consisting of a decision tree or forest, which are widely used in practice when either high interpretability or high accuracy are desired, respectively. For a single tree (axis-aligned or oblique), we show that the problem can be solved exactly and efficiently. For an ensemble of trees (a forest), such as random forests or gradient boosted trees, the problem is much harder and must be solved approximately. We give two algorithms that scale to large forests: one is very fast and also encourages the solution to be somewhat realistic; the other is slower but more accurate. This is joint work with my student Suryabhan Singh Hada.

Unix / Linux shell scripting is ubiquitous, partly due to the simplicity in which it allows combining third-party components (commands) written in any programming language. Unfortunately, this language-agnostic composition hinders automated parallelization, often forcing developers to manually rewrite shell scripts and their third-party components in other languages that support these features. In this talk I will present PaSh, a system for parallelizing Unix/Linux shell scripts. PaSh combines a just-in-time transcompiler that blends static pre-processing with dynamic interposition, a high-level annotation framework for expressing partial command specifications, and a collection of runtime primitives that support the execution of parallel shell scripts. PaSh achieves order-of-magnitude speedups on unmodified shell scripts, all while requiring no modifications to the system's underlying shell interpreter and while remaining virtually indistinguishable from Bash across the entire POSIX test suite. PaSh is worked on by several institutions, has received multiple awards, and is open-source software available by the Linux Foundation.

Low-level pointer-manipulating programs are hard to verify, requiring complex spatial program logics that support reasoning about aliasing and separation. Worse, when working over collections, these logics burden the programmer with annotating loops with quantified invariants that describe the contents of the collection. In this talk, I will give a demo of Flux, a static verifier for Rust that shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification for low-level imperative code. By factoring complex invariants into type constructors and simple refinements, Flux can efficiently synthesize loop annotations via liquid inference. We use a suite of vector-manipulating programs to demonstrate the advantages of Flux's refinement types over program logics, as implemented in the state-of-the-art Prusti verifier.

In this talk we will demonstrate that not only vulnerabilities in exposed services can be dangerous, but also the issue with leaving those services un-configured or with default credentials. We will also touch on the Devops side and talk about left over deployment artifacts that can disclose information and credentials about an infrastructure.

In this talk we will demonstrate that not only vulnerabilities in exposed services can be dangerous, but also the issue with leaving those services un-configured or with default credentials. We will also touch on the Devops side and talk about left over deployment artifacts that can disclose information and credentials about an infrastructure.

We study abstraction correspondences between hybrid trajectory semantics for verification and refinement, including discretization and state-based homomorphisms, simulations, bisimulations, preservations with progress, and show that they are all Galois connections. We investigate the problematic composition of hybrid state-based abstractions.

Smart contracts running on blockchains have been hailed as trustless platforms for carrying out agreements between parties without the risk of interference by the parties themselves or others. The immutability of such agreements is assumed to be a desirable feature, that is until the first bugs appear. In this talk, I will present ongoing work in building runtime verification tools for smart contracts, with a particular focus on recovery from discovered errors. In particular, I will discuss the use of runtime verification for smart contracts to handle (i) immutable specifications for mutable smart contracts; and (ii) recovery through smart contract design as long-lived transaction engines.

Spectre vulnerabilities violate our fundamental assumptions about programming abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about low-level hardware details such as speculative execution. I will explain the tradeoffs inherent in formal frameworks for Spectre, the complexity of defense tools, and the resulting security guarantees. I will also propose practical choices for developers of analysis and mitigation tools and identify interesting open problems in this area for future work.

Machine learning is a popular tool for building state of the art software systems. It is more and more used also in safety critical areas. This demands for verification techniques ensuring the safety and security of machine learning based solutions. However, in this presentation, we argue that the popularity of machine learning comes from the fact that no formal specification exists which renders traditional verification in appropriate. Instead, validation is typically demanded and we present a recent technique that validates certain correctness properties for an underlying recurrent neural network.

In this talk I will present some initial ideas (a first proposal) on how to define a framework to define missions for autonomous systems which are composed of different “controllers” that need to be active in different contexts. The idea is to try to be as formal as possible, to provide some kind of (semi-)formal reasoning, while being practical.

Dataflow languages have, as well as functional languages, immutable semantics, which is often implemented by copying values. A common compiler optimization known from functional languages involves analyzing which data structures can be modified in-place instead of copying them. In the presentation an algorithm to this so called Aggregate Update Problem for multi-clocked dataflow languages, i.e. those that allow streams to have events at disjoint timestamps, like e.g. Lucid, Lustre and Signal, is presented. Therefor TeSSLa, a generic stream transformation language with a small set of operators, is used to develop the ideas. Finally the empirical results of the implementation of the optimization into the TeSSLa compiler are presented.

In this talk I will present a paper published at TCC'21 together with Gianluca Brian and Daniele Venturi from Sapienza University of Rome. We study non-malleable secret sharing against joint leakage and joint tampering attacks. Our main result is the first threshold secret sharing scheme in the plain model achieving resilience to noisy-leakage and continuous tampering. The above holds under (necessary) minimal computational assumptions (i.e., the existence of one-to-one one-way functions), and in a model where the adversary commits to a fixed partition of all the shares into non-overlapping subsets of at most t−1 shares (where t is the reconstruction threshold), and subsequently jointly leaks from and tampers with the shares within each partition. We study the capacity (i.e., the maximum achievable asymptotic information rate) of continuously non-malleable secret sharing against joint continuous tampering attacks. In particular, we prove that whenever the attacker can tamper jointly with k>t/2 shares, the capacity is at most t−k. The rate of our construction matches this upper bound. An important corollary of our results is the first non-malleable secret sharing scheme against independent tampering attacks breaking the rate-one barrier (under the same computational assumptions as above).

Microarchitectural attacks are side/covert channel attacks which enable leakage/communication as a direct result of hardware optimizations. Secure computation on modern hardware thus requires hardware-software contracts which include in their definition of software-visible state any microarchitectural state that can be exposed via microarchitectural attacks. Defining such contracts has become an active area of research. In this talk, we will present leakage containment models (LCMs)—novel axiomatic hardware-software contracts which support formally reasoning about the security guarantees of programs when they run on particular microarchitectures. Our first contribution is an axiomatic vocabulary for formally defining LCMs, derived from the established axiomatic vocabulary used to formalize processor memory consistency models. Using this vocabulary, we formalize microarchitectural leakage—focusing on leakage through hardware memory systems—so that it can be automatically detected in programs. To illustrate the efficacy of LCMs, we first demonstrate that our leakage definition faithfully captures a sampling of (transient and non-transient) microarchitectural attacks from the literature. Next, we develop a static analysis tool, called Clou, which automatically identifies microarchitectural vulnerabilities in programs given a specific LCM. We use Clou to search for Spectre gadgets in benchmark programs as well as real-world crypto-libraries (OpenSSL and Libsodium), finding new instances of leakage. To promote research on LCMs, we design the Subrosa toolkit for formally defining and automatically evaluating/comparing LCM specifications.

Secure messaging applications are used by billions of users every day. Applications like WhatsApp make use of the seminal Signal protocol that provides conversation participants with end-to-end encryption guarantees. Due to the long-lived nature of messaging sessions, the threat of state exposure is more pronounced, and thus protocols like Signal regularly refresh keying material. In the cryptographic literature, many works address possible performance/security trade-offs beyond Signal and address additional problems like providing security against bad randomness generators and detecting active attacks. In this presentation, we examine this exciting line of work, discuss ongoing work and propose directions for further research. In particular we consider both the two-party setting and the more challenging group setting where parties may join and leave a group over time.

In this talk I will touch on two results I achieved during my PhD and Postdoc in the area of logics for algorithmic verification.

1. Integer linear arithmetic, also known as Presburger arithmetic, has been a central subject in computer science for many decades. A celebrated result by Ginsburg and Spanier show that the family of sets definable in Presburger arithmetic coincides with the family of semilinear sets. Despite more than fifty years of work on semilinear sets and several attempts, one question has remained unanswered: how do we efficiently compute the complement of a semilinear set? In a recent work with Chistikov and Haase, I answer this question by giving an optimal algorithm to compute such complements. As a corollary, this result gives a new way of deciding Presburger arithmetic optimally. Furthermore, our algorithm allows us to positively answer a conjecture by Pak and Nguyel on the VC dimension of Presbuger arithmetic [Combinatorica 39, 2019]. The VC dimension is a fundamental concept from Comptational Learning theory that can be applied to all first-order theories.

2. Separation logic is a well-known logic for the modular verification of pointer programs. An open problem in the area was how to design sound and complete proof systems for its assertion language, the major issue being that the multiplicative connectives of separation logic break all standard techniques used to prove completeness of axiom systems. In a paper published at CSL'20, I showed how to handle this issue, and derived the first sound and complete proof system for a separation logic featuring both multiplicative connectives (the so called separating conjunction and the separating implication). Completeness is shown with a model theoretical technique that is reusable in practice, and that can be adapted to tackle complexity questions.

After a round-up on the aforementioned results, I will move to my current research project, that aims at developing proof techniques and algorithms to mathematically prove the presence of arithmetic errors (e.g., buffer and integer overflows) in programs.

Serverless has emerged as the next dominant cloud architecture and paradigm due to its scalability and a flexible billing model. In serverless, developers structure their cloud services as a set of functions connected in a workflow, whereas providers take responsibility for dynamically scaling each function’s resources. This labor division opens opportunities for systems researchers to innovate in serverless computing. However, leading serverless providers, like AWS Lambda, rely on proprietary infrastructure ill-suited for systems research in academia.

The Cardano blockchain underlies one of the world's top-ten cryptocurrencies, and supports smart contracts written in Haskell, which work very differently from those on the Ethereum Virtual Machine (the largest smart contract platform). While some vulnerabilities are fixed as a result, it is still possible in principle for large sums to be stolen, or simply lost, due to bugs in smart contracts. Testing smart contracts thoroughly is thus of paramount importance. QuickCheck is a 'property-based testing' tool, that generates random test cases and validates observed system behaviour against a kind of formal specification. But what should a formal specification of a smart contract look like? Quviq has been developing a QuickCheck-based test framework for these smart contracts. I'll talk about the framework itself, and some of the challenges we have addressed, and which remain to be addressed.

Despite significant efforts on cybersecurity, we are observing an increasing number of attacks in recent years. The reason for this harsh reality is all our efforts aim at individual incidents and there is no deep understanding of attack surfaces in software systems. As a result, software systems are integrated with too many individual patches and ad-hoc mitigations, which introduces unacceptable overhead but not substantial security benefits. In this talk, I will present a systematic approach to understanding attack surfaces. This approach provides security analysts and developers with the ability to quantify the impact of attack surfaces and facilitate the development of universal and effective defense solutions. Technically, this approach consists of two steps - induction and deduction. The induction step summarizes the security incident and abstracts the essential attack surface behind the incident. The deduction step generalizes the essential attack surface to different systems and applies it in the exploitation of different error types. By mitigating the generalized attack surface, the developers can design universal protections. In this talk, I will illustrate this research approach starting from a security incident in the Linux kernel. I will present a universal and effective defense that mitigates the generalized attack surface and is widely adopted in various commodity Operating System kernels. In the future, I plan to further advance this systematic approach and make it a fundamental part of the entire software development lifecycles. More specifically, I will: 1) enrich induction and deduction techniques for more attack forms under new contexts, 2) formalize the description of attack surfaces, and 3) quantify the security of systems to optimize and re-construct existing defenses architecture.

Multithreaded concurrency is an extremely challenging programming setting, with bugs manifesting themselves in resource starvation and atomicity violations. While there have been efforts to simplify concurrent programming through higher-level programming abstractions, developers tend to choose low-level concurrent programming abstractions (with locks and condition variables as synchronization primitives) due to efficiency issues. This talk will present my recent work on bridging this efficiency vs. programmability trade-off in concurrent programming by employing lightweight formal methods in the compiler. Given a concurrent program implemented in a higher-level programming abstraction, our approach automatically synthesizes efficient and correct-by-construction code implemented in terms of standard synchronization primitives. Specifically, the first part of the talk will demonstrate how to synthesize all necessary signaling operations, and the second part will illustrate how to synthesize a fine-grained locking scheme that maximizes parallelism. As I will demonstrate through empirical results, this approach notably simplifies concurrent programming while achieving optimal performance.

Digital technology creates risks to people's privacy in ways that did not exist before. I design end-to-end private systems to mitigate these real-world privacy risks. In this talk I will discuss my designs for two applications. These applications highlight key aspects of my work: I analyse security, privacy, and deployment requirements; and address these requirements by designing new cryptographic primitives and system architectures. In the first part of this talk, I will focus on my DP-3T and CrowdNotifier designs for digital proximity and presence tracing that help mitigate the COVID-19 pandemic. These designs combine novel cryptographic primitives and communication systems to protect users’ privacy. The DP3T and CrowdNotifier designs have been deployed to millions of phones. In the second part of this talk, I will present DatashareNetwork, a document search system for investigative journalists that enables them to locate relevant documents for their investigations. DatashareNetwork combines a novel multi-set private set intersection primitive with anonymous communication and authentication systems to create a decentralised and privacy-friendly document search system.

We study the generalization properties of the popular stochastic optimization method known as stochastic gradient descent (SGD) for optimizing general non-convex loss functions. Our main contribution is providing upper bounds on the generalization error that depend on local statistics of the stochastic gradients evaluated along the path of iterates calculated by SGD. The key factors our bounds depend on are the variance of the gradients (with respect to the data distribution) and the local smoothness of the objective function along the SGD path, and the sensitivity of the loss function to perturbations to the final output. Our key technical tool is combining the information-theoretic generalization bounds previously used for analyzing randomized variants of SGD with a perturbation analysis of the iterates.

Standard hybrid encryption schemes based on the KEM-DEM framework are hard to implement efficiently in a distributed manner while maintaining the CCA security property of the scheme. This is because the DEM needs to be decrypted under the key encapsulated by the KEM, before the whole ciphertext is declared valid. In this paper we present a new variant of the KEM-DEM framework, closely related to Tag-KEMs, which sidesteps this issue. We then present a post-quantum KEM for this framework based on Learning-with-Rounding, which is designed specifically to have fast distributed decryption. Our combined construction of a hybrid encryption scheme with Learning-with-Rounding based KEM, called Gladius, is closely related to the NIST Round 3 candidate called Saber. We wrote prototype distributed implementation that achieves a decapsulation time of 4.99 seconds for three parties.

Consider a distributed protocol whose n processes ensure some (distributed) safety and liveness properties, communicating with each other without synchrony, despite a certain the number t of Byzantine processes. It has been known for decades that such distributed protocols cannot ensure safety as soon as more than a threshold of t_0 processes fail, typically one third of the processes.

By contrast, only recently did the community discover that some of these distributed protocols can be made accountable by ensuring that correct processes detect at least t_0 + 1 faulty processes responsible of any safety violation. This is particularly surprising (and positive) given that accountability is a powerful tool to mitigate safety violations in distributed protocols. Indeed, exposing crimes and punishments naturally incentivizes exemplarity.

We propose a generic transformation of any distributed protocol into an accountable version of this protocol. First, we partition the commission faults into two classes: the equivocation faults and the evasion faults and illustrate why the former are are easier and less cumbersome to detect than the latter. Our transformation builds upon the secure broadcast primitive in a way ensuring that every safety violation is necessarily a consequence of equivocation faults.

Due to the secure broadcast primitive, our transformation increases the communication and message complexities of the original distributed protocol by an O(n^2) multiplicative factor in the worst case.

We revisit the problem of designing light-client blockchain protocols from the perspective of classical proof-system theory. This results in a framework that allows quantifying the security guarantees provided to a light-client verifier even when interacting only with a single dishonest (full-node) prover. We define a new primitive called succinct non-interactive argument of chain knowledge (SNACK) capturing this intuition and show how augmenting any blockchain with a graph-labeling proof of sequential work (GL-PoSW) enables SNACK proofs for this blockchain. We also provide a unified and extended definition of GL-PoSW covering all existing constructions and describe a new variant. We then show how SNACKs can be used to construct light-client protocols, and highlight some deficiencies of existing solutions. (Joint work with: Georg Fuchsbauer, Peter Gazi, and Karen Klein)