This session will feature short talks by faculty from the MIT Department of Electrical Engineering and Computer Science on trustworthy systems.

Adam Chlipala, Correct-by-Construction Cryptographic Software: Important cryptographic algorithms have many different variations for different parameters and target hardware platforms, and conventionally, expert engineers need to reimplement an algorithm for each such combination, to get good performance.  The Fiat Cryptography project provides a generator that automates that specialization work that was previously highly manual.  As a bonus, the Fiat Cryptography code generator has a machine-checked mathematical proof of correctness.  It has been adopted to produce parts of a number of popular open-source libraries.

Srini Devadas, Security With Minimal Trust: We describe an approach to build computing systems that provide integrity of computation and data privacy for users while minimizing software and hardware that needs to be trusted.

Frans Kaashoek, Verifying Distributed Systems With Concurrent Separation Logic: Distributed systems are at the heart of cloud computing and bugs in them can lead to outages of Web sites. Unfortunately distributed systems are hard to get right because they must handle concurrency, crash recovery, replication, and reconfiguration, which interact in subtle ways.  A promising approach to verifying such systems (and thereby systematically eliminating bugs) is based on concurrent separation logic, which allows components to be verified independently yet handle tricky interaction between components.

Mengjia Yan, Principled Hardware Defenses Against Side-channel Attacks: We will talk about the development of a dedicated security evaluation framework for early-stage microarchitectural defenses against speculative execution attacks. Amidst the ongoing cat-and-mouse game between hardware attacks and defenses, our framework can assist computer architects in formulating principled responses to the evolving landscape of hardware threats.

Part of the Expanding Horizons in Computing IAP series presented by the MIT Schwarzman College of Computing. See the full list of activities at computing.mit.edu/ExpandingHorizons.