Automated verification for system software

Unmet Need: Efficient system software verification

Current approaches to software verification are hampered by the sheer size and complexity of modern systems. These challenges not only impede efficient verification but also lack cost-effective solutions.

The Technology: Time and cost-efficient way to verify system code

This system aims to streamline system software verification at a reduced cost. It enables software verification without the need for manual modifications beforehand and simplifies the integration of manually crafted layer specifications and refinement proofs, automating the verification process for system software. Spoq required 70% less proof effort while ensuring the correctness of the unmodified implementation that was directly compiled and executed. Spoq offers a significant improvement in the efficiency of verifying system software, potentially enhancing the security of computer systems.

Applications:

Diagnostic framework for software vulnerability
Research tool for software design/code translation
Integrated framework for software security services

Advantages:

Cost-effective
Automated framework
No prior manual modification required
Support full C semantics
Facilitates integration of manually written code

Lead Inventor:

Jason Nieh, Ph.D.

Patent Information:

Patent Pending

Related Publications:

Li, X., Li, X., Qiang, W., Gu, R.,Nieh, J. “Spoq: Scaling Machine-Checkable Systems Verification in Coq” 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23). 2023: 851-869.

Tech Ventures Reference:

IR CU23360
Licensing Contact: Greg Maskel