Datatype Generic Packet Descriptions

Friday, June 02, 2017

Abstract: Complex protocols describing the communication or storage of binary data are difficult to describe precisely. In this talk, I want to explore how to define data types describing a binary data formats and generate the corresponding serialization and deserialization functions from such descriptions. By embedding these data types in a general purpose dependently typed […]

Read More

Rust: from POPL to practice

Tuesday, February 07, 2017

Abstract: In 2015, a language based fundamentally on substructural typing–Rust–hit its 1.0 release, and less than a year later it has been put into production use in a number of tech companies, including some household names. The language has started a trend, with several other mainstream languages, including C++ and Swift, in the early stages […]

Read More

Tech Talk: E3DB – Tozny’s End-to-End Encrypted Database

Wednesday, December 07, 2016

abstract: Project E3DB is a tool for programmers who want to build an end-to-end encrypted database with sharing into their projects. We are providing a command-line client for you to play with and a Java SDK to prototype with. Over the next few weeks, we’ll be getting feedback from you, adding features, and making it […]

Read More

Tech talk: Verified Secure Computing using Trusted Hardware

Thursday, September 29, 2016

abstract: Security-critical applications constantly face threats from exploits in lower computing layers such as the OS and Hypervisor, or even attacks from malicious administrators. To protect sensitive data from such privileged adversaries, there is increasing development of secure hardware primitives, such as Intel SGX. Intel SGX instructions enable user mode applications to package trusted code […]

Read More

Tech talk: Internet of Things: From Small- to Large-Scale Orchestration

Tuesday, August 30, 2016

abstract: The domain of Internet of Things (IoT) is rapidly expanding beyond research and becoming a major industrial market with such stakeholders as major manufacturers of chips and connected objects, and fast-growing operators of low-power wide-area networks. Importantly, this emerging domain is driven by applications that leverage the infrastructure to provide users with innovative, high-value […]

Read More

Tech Talk: Hoare Monitor Programming Revisited : Safe and Optimized Concurrency

Tuesday, July 12, 2016

abstract: Hoare monitors, invented by Brinch Hansen and Hoare in 1973, are widely used to safely handle concurrent programming in different languages ranging from C++11 to Tower, an EDSL developed by Galois as part of the High-Assurance Cyber Military Systems (HACMS) DARPA program. This talk will explain how basic safety properties are assured using Tower, […]

Read More

Tech talk: Interrupts in OS code: let’s reason about them. Yes, this means concurrency.

Wednesday, May 04, 2016

abstract: Existing modeled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where […]

Read More

Tech talk: Adversarial Machine Learning, Privacy, and Cybersecurity in the Age of Data Science

Friday, March 25, 2016

abstract: Due to the exponential growth of our ability to collect, centralize, and share data in recent years we have been able tackle problems previously assumed to be insurmountable. Ubiquitous sensors, fast and efficient machine learning, and affordable commercial-off-the-shelf technologies have not only deepened our understanding of our world, but also democratized these capabilities. As […]

Read More

Tech talk: Toward Extracting Monadic Programs from Proofs

Friday, March 18, 2016

abstract: The Curry-Howard Isomorphism motivates the well known proofs-as-programs interpretation. Under that interpretation, sufficiently different proofs yield different programs. This work is a step toward extracting monadic programs from proofs. In working with the list monad as a motivating example, we discovered that the standard type bind (M a -> (a -> M b) -> […]

Read More