National HCSS Conference 2014

14th Annual High Confidence Software and Systems Conference.
file

Visible to the public The Cyber-Physical Limits of Control

Abstract

As the speed of computer systems and their integration with the physical world have grown, the physical limits of control have become increasingly relevant for ensuring high confidence in software systems. In this talk, I will present exciting recent results on the physical limits in space and time for realizing optimal coordination and control in cyber-physical systems, and discuss their implications for the future of reasoning about control.

Speaker Bio

file

Visible to the public Cryptol version 2: An Open Source Cryptol

Abstract

HCSS participants, in the main, know about Galois' Cryptol language and system and its capabilities. In short, Cryptol is a domain-specific language for programming, executing, testing, and formally reasoning about streams of bits. Cryptol particularly excels at specifying and reasoning about cryptographic algorithms.

Galois has decided to "reboot" Cryptol and create, from the ground up, a new Open Source Cryptol release: Cryptol version 2.

file

Visible to the public Using Coq to Verify DPLL

Abstract

Most large software systems have complex data structures with complex invariants. Many bugs can be traced to code that does not maintain these invariants. As an example, the Heartbleed bug can be traced to an attacker sending a packet that violates an invariant that is assumed to be true in the OpenSSL code. Often these invariants are not well documented. However, maintaining them is necessary for correct operation of the software.