FMS 2018 – Proceedings

Message from the Chairs
Welcome to the 2nd Workshop on Formal Methods and Security (FMS), co-held with PLDI 2018, on June 18, 2018. While the fields of security and privacy and of formal methods/programming languages are thriving areas of computer science, the communities tend to be mostly disjoint. Though there are several formal techniques used for ensuring security, there is no systematic use of emerging powerful formal techniques in the real world to ensure security and privacy. The goal of this workshop is to bring together researchers from both communities in order to have them learn about the important problems and relevant techniques in each field, to foster collaboration leading to applying “cutting edge” formal techniques in security.

A Recursive Strategy for Symbolic Execution to Find Exploits in Hardware Designs
Rui Zhang and Cynthia Sturton
(University of North Carolina, USA)
This paper presents hardware-oriented symbolic execution that uses a recursive algorithm to find, and generate exploits for, vulnerabilities in hardware designs. We first define the problem and then develop and formalize our strategy. Our approach allows for a targeted search through a possibly infinite set of execution traces to find needle-in-a-haystack error states. We demonstrate the approach on the open-source OR1200 RISC processor. Using the presented method, we find, and generate exploits for, a control-flow bug, an instruction integrity bug and an exception related bug.

Publisher's Version

FMS 2018 – Proceedings

2018 ACM SIGPLAN International Workshop on Formal Methods and Security (FMS 2018)