Powered by
2018 ACM SIGPLAN International Workshop on Formal Methods and Security (FMS 2018),
June 18, 2018,
Philadelphia, PA, USA
2018 ACM SIGPLAN International Workshop on Formal Methods and Security (FMS 2018)
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.
@InProceedings{FMS18p1,
author = {Rui Zhang and Cynthia Sturton},
title = {A Recursive Strategy for Symbolic Execution to Find Exploits in Hardware Designs},
booktitle = {Proc.\ FMS},
publisher = {ACM},
pages = {1--9},
doi = {10.1145/3219763.3219764},
year = {2018},
}
Publisher's Version
proc time: 0.22