Research Groups

 As an increasingly large part of our identity moves online, there are many technical concerns surrounding the security and reliability of these systems: is our privacy being protected from third-party advertisers, online criminals, or even state-level actors? Can we depend on these systems to be available when we need them, and be easy enough to manage even as they grow to meet Internet-scale demand?

Our group builds and studies tools, techniques, and abstractions that help solve these and other real-world problems in network systems and security. Our work spans a broad range of topics, from the security of physical keys to building robust distributed systems using software-defined networks and other virtualization technologies. We have helped design systems that can leverage emerging architecture trends such as SoC (System-on-Chip) FPGA integration in mobile environments, as well as developed new protocols and tools that enable users to circumvent their government’s Internet censorship.

Bugs in hardware and software may have serious repercussions on our work and even our safety. At the same time, the rapid obsolescence of electronic designs demands high productivity. For these reasons formal methods have become an essential ingredient of design flows. Our work focuses on improving the productivity of programmers and system designers by developing methods and tools that make it easier to design and verify reliable software and hardware. Our research efforts are concentrated in four areas. The first area is program verification, where we develop techniques for automatically proving correctness of programs. Current focus is on verifying that a given software is secure, and on learning from large collections of programs. The second research area is program synthesis. Its goal is to develop techniques for synthesizing programs and circuits from programmer insights provided in a variety of styles (code snippets, declarative specifications, example scenarios). Current application areas for this work include programs for software-defined networking, and device drivers.  The third research area is model checking, which is an approach to verification that lends itself to a high degree of automation. Over the years our group has developed model checkers like vis and iimc. Current emphasis is on verification of parameterized systems.  The fourth area is the decision procedures that are at the heart of the verification engines, notably SAT and SMT solvers, and Binary Decision Diagrams.