Automated Reasoning for Software/Systems Quality and Security

(CSE Distinguished Lecture Series)

Nadia Polikarpova, Sean Gao and Deian Stefan
CSE Professors
Monday, October 9, 2017, 11am
Room 1202, CSE Building

Recently CSE faculty hires (l-r) Nadia Polikarpova, Sicun (Sean) Gao, and Deian Stefan will jointly present their research on automated reasoning for software and systems quality and security.

Automated Reasoning for Software/Systems Quality and Security

Each of the three CSE faculty members will speak for about 20 minutes on their respective topics below:

1. Nadia Polikarpova: Type-Driven Program Synthesis 

Modern programming languages safeguard developers from many typical errors, yet more subtle errors still plague software. Program synthesis has the potential to eliminate such errors, by generating executable code from concise and intuitive high-level specifications. This talk will present Synquid, a program synthesizer that accepts specifications in the form of expressive types and uses a specialized type checker to validate large sets of candidate programs at once, whereby efficiently pruning the search space. Synquid is the first synthesizer powerful enough to automatically discover provably correct implementations of complex data structure manipulations, such as insertion into Red-Black Trees and AVL Trees, and normal-form transformations on propositional formulas. Each of these programs is synthesized in under a minute. 

2. Sicun Gao: Automated Reasoning for Physical Computing 

Automated reasoning is an area of AI that studies algorithmic approaches to logical reasoning and (NP-hard) problem solving in general. My research focuses on automated reasoning for cyber-physical systems (e.g. autonomous cars) that exhibit complex behaviors because of their tight integration of discrete and continuous components. I will describe how an automated reasoning framework can tackle the core computational challenges in this domain, by unifying a variety of algorithms from combinatorial search, numerical optimization, and statistical learning.

3. Deian Stefan: Physis: A Secure Runtime System for Physically-Coupled Devices

Building IoT applications that are secure and preserve data privacy is notoriously difficult. Though the popular media and some researchers have been quick to attribute fault to IoT developers, this fault placement is misguided. IoT developers are tasked with the heroic task of building secure applications that not only interact with the physical world, but are distributed and run on heterogeneous devices. Unfortunately, existing programming models do not make
most these concerns explicit and force developers to devise ad-hoc mechanisms to, for example, deal with data privacy. Unsurprisingly, this has led to scenarios where sensitive sensor data have been leaked and devices have been exploited to participate in distributed denial-of-service (DDOS) attacks.

In this talk, I will describe a language-based approach to building secure and privacy-preserving application. In particular, I will describe our new efforts to develop a language runtime system, called Physis, that will enforce security and data privacy for IoT applications.  At the heart of Physis is a novel information flow control monitor that tracks and restricts the flow of information at abstraction boundaries (e.g., physical-software boundary and the
network-application boundary) and a physically-coupled contract system that allows developers to specify high-level security and privacy policies. Together, these mechanisms will allow developers to build application that are uniformly resilient to physical and cyber attacks, while still capable of performing necessary (and privacy-aware) operations, such as sensing, actuation, and network communication.