A Unified View of Weirdness: A Logical Framework for Emergent Execution

ABSTRACT

For any software application, there are multiple worlds relevant to modeling emergent execution (see inset figure). The design-level world re ects programmer intentions and language abstractions, the binary world reflects the concrete representations of these abstractions, and the platform world reflects the ground truth of this application in operation. These worlds are distinct, but they are also closely inter-related and interdependent, and, in our view, weirdness (in the sense of weird machines [1, 2]) derives from being rudely awakened to these facts. Formal methods and models for emergent execution are clearly required [3] to detect potential emergent execution and to develop effective countermeasures. However, state-of-the-art formal methods tools for software -- i.e., everything from language semantics and program logics to practical analysis tools|take a monolithic "one world" view of software that can express intra-world properties but not inter-world properties. What is required is a foundation for formal methods that allows for expression of both intra- and inter-world properties.

This talk describes ongoing research at Two Six Technologies and Binarly using dis- tributed logics [4, 5] as a unifying framework for formal analysis of emergent execution in the setting of UEFI (Unified Extensible Firmware Interface) boot loaders. Distributed logics are multi-world modal logics in which worlds ("local logics") are related via special inter-logic modalities called distributions; we are particularly focused on applying Simulation Logic [5] in this context. Local logics in the UEFI setting include Incorrectness Logics [6] and Adversary Logic [7] for establishing the existence of vulnerable execution paths in binary and platform worlds and inter-relating these with design-level source code abstractions. These logics are mechanized in Coq using a modal logics framework of Benzmüller and Paleo [8] and we are using a recently published formal semantics for P-Code [9] as a exible basis for reasoning about binaries.

Author

Dr William Harrison received his BA in Mathematics from Berkeley in 1986 and his doctorate from the University of Illinois at Urbana-Champaign in 2001 in Computer Science. From 2000-2003, he was a post-doctoral research associate at the Oregon Graduate Institute in Portland, Oregon. Until recently, Dr Harrison was on the faculty in the Electrical Engineering and Computer Science department at the University of Missouri. Currently, he is a Senior Principal Research Scientist at Two Six Technologies, Inc., transitioning his research on high assurance hardware into practice. His research interests include all aspects of programming languages research (e.g., language-based computer security, semantics, design and implementation), reconfigurable computing, formal methods and malware analysis.

 

References

[1] Thomas Dullien. Weird Machines, Exploitability, and Provable Unexploitability. IEEE Transactions on Emerging Topics in Computing, 8(2):391-403, 2020.

[2] Jennifer Paykin, Eric Mertens, Mark Tullsen, Luke Maurer, Benoit Raziet, , and Scott Moore. Weird Machines as Insecure Compilation. In Workshop on Foundations of Computer Security (FCS), 2019.

[3] Sergey Bratus and Anna Shubina. Exploitation as code reuse: On the need of formalization. Inf. Technol., 59(2):93, 2017.

[4] Gerard Allwein, William Harrison, and David Andrews. Simulation Logic. Logic and Logical Philosophy, 23(3):277-299, Sep. 2013.

[5] Gerard Allwein and William L. Harrison. Distributed Modal Logic. In Katalin Bimb o, editor, J. Michael Dunn on Information Based Logics, pages 331-362. Springer International Publishing, 2016.

[6] Peter W. O'Hearn. Incorrectness Logic. Proc. ACM Program. Lang., 4(POPL), dec 2019.

[7] Julien Vanegue. Adversarial Logic. In Static Analysis: 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5-7, 2022, Proceedings, page 422-448, 2022.

[8] Christoph Benzmuller and Bruno Woltzenlogel Paleo. Interacting with Modal Logics in the Coq Proof Assistant. In Computer Science - Theory and Applications, pages 398-411. Springer International Publishing, 2015. [

9] Nico Naus, Freek Verbeek, and Binoy Ravindran. A Formal Semantics for P-Code. In 14th International Conference on Veri ed Software: Theories, Tools, and Experiments (VSTTE'22), 2022.

*This research was developed with funding from the Defense Advanced Research Projects Agency (DARPA). The views, opinions and/or ndings expressed are those of the author and should not be in- terpreted as representing the o cial views or policies of the Department of Defense or the U.S. Government.

Distribution Statement `A' (Approved for Public Release, Distribution Unlimited)