Mechanizing the Metatheory of the ReWire Language with Applications to Code Vulnerability
Abstract
This research considers a formal verification approach to the detection and mitigation of code vulnerability in ReWire programs. Strategies: (1) Encoding of distributed logic in the Coq theorem proving system; (2) Verification of the ReWire complier in the Coq theorem proving system.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- May 18, 2016
- Source ID
- N00173161G004
Entities
People
- William L. Harrison
Organizations
- Curators of the University of Missouri
- United States Naval Research Laboratory
- United States Navy