ABSTRACT. Formal reasoning about programs is one of the oldest and most fundamental research directions in computer science. It has also been one of the most elusive. There has been a tremendous amount of valuable research in formal  methods, but rarely have formal reasoning techniques been deployed as part of the development process of large industrial codebases.

This talk describes work in continuous reasoning, where formal reasoning about a (changing) codebase is done in a fashion which mirrors the iterative, continuous model of software development that is increasingly practiced in industry. We suggest that advances in continuous reasoning will allow formal reasoning to scale to more programs, and more programmers. We describe our experience using continuous reasoning with large, rapidly changing codebases at Facebook, and we describe open problems and directions for research for the scientific community.

This a paper with the same title accompanying this talk appears in the LICS’18 proceedings.

ABSTRACT.   Passwords are still the most widespread means for authenticating
  users, even though they have been shown to create huge security
  problems. This motivated the use of additional authentication
  mechanisms used in so-called multi-factor authentication
  protocols. In this paper we define a detailed threat model for this
  kind of protocols: while in classical protocol analysis attackers
  control the communication network, we take into account that many
  communications are performed over TLS channels, that computers may
  be infected by different kinds of malwares, that attackers could
  perform phishing, and that humans may omit some actions. We
  formalize this model in the applied pi calculus and perform an
  extensive analysis and comparison of several widely used protocols
  --- variants of Google 2 Step and FIDO's U2F. The analysis is completely
  automated, generating systematically all combinations of threat
  scenarios for each of the protocols and using the Proverif tool for
  automated protocol analysis. Our analysis highlights weaknesses and
  strengths of the different protocols, and allows us to suggest
  several small modifications of the existing protocols which are easy
  to implement, yet improve their security in several threat scenarios.

ABSTRACT. We present composition theorems for security protocols, to compose a key exchange protocol and a symmetric-key protocol that uses the exchanged key. Our results rely on the computational model of cryptography and are stated in the framework of the tool CryptoVerif. They support key exchange protocols that guarantee injective or non-injective authentication. They also allow random oracles shared between the composed protocols. To our knowledge, they are the first composition theorems for key exchange stated for a computational protocol verification tool, and also the first to allow such flexibility.

As a case study, we apply our composition theorems to a proof of TLS 1.3 Draft-18. This work fills a gap in a previous paper that informally claims a compositional proof of TLS 1.3, without formally justifying it.

ABSTRACT. Cryptographic channels aim to enable authenticated and confidential communication over the Internet. The general understanding seems to be that providing security in the sense of authenticated encryption for every (unidirectional) point-to-point link suffices to achieve this goal. As recently shown (in FSE17/ToSC17), however, even in the bidirectional case just requiring the two unidirectional links to provide security independently of each other does not lead to a secure solution in general. Informally, the reason for this is that the increased interaction in bidirectional communication may be exploited by an adversary. The same argument applies, a fortiori, in a multi-party setting where several users operate concurrently and the communication develops in more directions. In the cryptographic literature, however, the targeted goals for group communication in terms of channel security are still unexplored.

Applying the methodology of provable security, we fill this gap by (i) defining exact (game-based) authenticity and confidentiality goals for broadcast communication and (ii) showing how to achieve them. Importantly, our security notions also account for the causal dependencies between exchanged messages, thus naturally extending the bidirectional case where causal relationships are automatically captured by preserving the sending order. On the constructive side we propose a modular and yet efficient protocol that, assuming only reliable point-to-point links between users, leverages (non-cryptographic) broadcast and standard cryptographic primitives to a full-fledged broadcast channel that provably meets the security notions we put forth.

ABSTRACT. Architectural isolation can be used to secure computation on a remote secure processor with a private key where the privileged software is potentially malicious as recently deployed by Intel's Software Guard Extensions (SGX). This talk will first describe the Sanctum secure processor architecture, which offers the same promise as SGX, namely strong provable isolation of software modules running concurrently and sharing resources, but protects against an important class of additional software attacks that infer private information by exploiting resource sharing.

The talk will then describe a verification methodology based on a trusted abstract platform (TAP) that formally models idealized enclaves and a parameterized adversary. Machine-checked proofs show that the TAP satisfies the three key security properties needed for secure remote execution: integrity, confidentiality and secure measurement. Machine-checked proofs also show that SGX and Sanctum are refinements of the TAP under certain parameterizations of the adversary, demonstrating these systems implement secure enclaves for the stated adversary models.

Biography:

Srini Devadas is the Webster Professor of Electrical Engineering and Computer Science at the Massachusetts Institute of Technology (MIT) where he has been on the faculty since 1988. Devadas's research interests span Computer-Aided Design (CAD), computer security and computer architecture. He is a Fellow of the IEEE and ACM. He has received a 2014 IEEE Computer Society Technical Achievement award, the 2015 ACM/IEEE Richard Newton technical impact award, and the 2017 IEEE Wallace McDowell award for his research. Devadas is a MacVicar Faculty Fellow and an Everett Moore Baker teaching award recipient, considered MIT's two highest undergraduate teaching honors.

ABSTRACT. Attack trees are a well-recognized formalism for security modeling and analysis, but in this work we tackle a problem that has not yet been addressed by the security or formal methods community – namely guided design of attack trees. The objective of the framework presented in this paper is to support a security expert in the process of designing a pertinent attack tree for a given system. In contrast to most of existing approaches for attack trees, our framework contains an explicit model of the real system to be analyzed, formalized as a transition system that may contain quantitative information. The leaves of our attack trees are labeled with reachability goals in the transition system and the attack tree semantics is expressed in terms of traces of the system. The main novelty of the proposed framework is that we start with an attack tree which is not fully refined and by exhibiting paths in the system that are optimal with respect to the quantitative information, we are able to suggest to the security expert which parts of the tree contribute to optimal attacks and should therefore be developed further. Such useful parts of the tree are determined by solving a satisfiability problem in propositional logic.