Automated verification for system software

This technology called Spoq, Scaling Machine-Checkable Systems Verification in Coq, is an automated verification framework 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