Wednesday, June 4, 2025
LBNN
  • Business
  • Markets
  • Politics
  • Crypto
  • Finance
  • Energy
  • Technology
  • Taxes
  • Creator Economy
  • Wealth Management
  • Documentaries
No Result
View All Result
LBNN

New tool automates the formal verification of systems software

Simon Osuji by Simon Osuji
October 30, 2023
in Artificial Intelligence
0
New tool automates the formal verification of systems software
0
SHARES
6
VIEWS
Share on FacebookShare on Twitter


New tool automates the formal verification of systems software
Tang Family Assistant Professor of Computer Science Rongui Gu (left) and Professor of Computer Science Jason Nieh (right). Credit: Columbia Engineering

Formal systems verification, which mathematically proves that code is secure in all circumstances, is a relatively new technology. Software is getting more complex and harder to get right using traditional software testing techniques. Making software correct, safe, and secure is becoming even more critical as the use of generative AI techniques like ChatGPT to automatically write programs increases. In fact, there will be even more need for verification to ensure those automatically generated programs are correct.

Related posts

AI deployemnt security and governance, with Deloitte

AI deployemnt security and governance, with Deloitte

June 4, 2025
AI enables shift from enablement to strategic leadership

AI enables shift from enablement to strategic leadership

June 3, 2025

Recent work directed by professors Ronghui Gu and Jason Nieh introduced a new tool, Spoq, that significantly reduces the complex efforts people must use to verify real-world software and makes it possible to verify existing C systems code without modifications.

Formal verification offers a systematic and rigorous approach to software and hardware verification, helping to ensure that systems behave correctly and meet their intended specifications. With Spoq, many aspects of formal verification can be automated, significantly reducing manual proof efforts for verification. The paper was presented at the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI) Conference on July 12, 2023.

System software forms the software foundations of our computing infrastructure. Modern system software is large, complex, and imperfect, with vulnerabilities that can be exploited to compromise the security of a system. Formal verification offers a potential solution to this problem by mathematically proving that system software can provide critical security guarantees. Unfortunately, it remains too difficult and requires too much human effort to apply in practice.

Previous tools developed by Nieh’s and Gu’s teams introduced verification techniques to make certain proofs possible that could not have been done before. Spoq’s key feature is that it automates the tedious and time-consuming parts of many proofs. “Spoq can generate results in about an hour compared to doing it manually, which can take months or years to formally verify a system,” says Xupeng Li, the paper’s lead author and a Ph.D. student with both Nieh and Gu.

Over the next few months, the lab is focused on making Spoq open-source so that formal verification can be widely deployed to secure the foundations of our computing infrastructure’s software.

The study is titled “Spoq: Scaling Machine-Checkable Systems Verification in Coq.”

More information:
Study: www.usenix.org/conference/osdi … esentation/li-xupeng

Provided by
Columbia University School of Engineering and Applied Science

Citation:
New tool automates the formal verification of systems software (2023, October 30)
retrieved 30 October 2023
from https://techxplore.com/news/2023-10-tool-automates-formal-verification-software.html

This document is subject to copyright. Apart from any fair dealing for the purpose of private study or research, no
part may be reproduced without the written permission. The content is provided for information purposes only.





Source link

Previous Post

African Court on Human and Peoples’ Rights (ACHPR) Press Release on the Situation in the Gaza Strip

Next Post

Max Q: ABL Space nears next launch

Next Post
Max Q: ABL Space nears next launch

Max Q: ABL Space nears next launch

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

RECOMMENDED NEWS

Space Force seeks orbital-refueling tech in new budget

Space Force seeks orbital-refueling tech in new budget

1 year ago
Libyan youth call for sustainability of the ceasefire agreement and inclusion in state building

Libyan youth call for sustainability of the ceasefire agreement and inclusion in state building

4 months ago
Pre-Symposium Event Highlights Infrastructure Opportunities Ahead of Sustainable Infrastructure Development Symposium of South Africa (SIDSSA) 2024

Pre-Symposium Event Highlights Infrastructure Opportunities Ahead of Sustainable Infrastructure Development Symposium of South Africa (SIDSSA) 2024

1 year ago
2023 Mansfield-Ruddock Art Prize: Olubunmi Agusto Emerges Winner

2023 Mansfield-Ruddock Art Prize: Olubunmi Agusto Emerges Winner

2 years ago

POPULAR NEWS

  • Ghana to build three oil refineries, five petrochemical plants in energy sector overhaul

    Ghana to build three oil refineries, five petrochemical plants in energy sector overhaul

    0 shares
    Share 0 Tweet 0
  • When Will SHIB Reach $1? Here’s What ChatGPT Says

    0 shares
    Share 0 Tweet 0
  • Matthew Slater, son of Jackson State great, happy to see HBCUs back at the forefront

    0 shares
    Share 0 Tweet 0
  • Dolly Varden Focuses on Adding Ounces the Remainder of 2023

    0 shares
    Share 0 Tweet 0
  • US Dollar Might Fall To 96-97 Range in March 2024

    0 shares
    Share 0 Tweet 0
  • Privacy Policy
  • Contact

© 2023 LBNN - All rights reserved.

No Result
View All Result
  • Home
  • Business
  • Politics
  • Markets
  • Crypto
  • Economics
    • Manufacturing
    • Real Estate
    • Infrastructure
  • Finance
  • Energy
  • Creator Economy
  • Wealth Management
  • Taxes
  • Telecoms
  • Military & Defense
  • Careers
  • Technology
  • Artificial Intelligence
  • Investigative journalism
  • Art & Culture
  • Documentaries
  • Quizzes
    • Enneagram quiz
  • Newsletters
    • LBNN Newsletter
    • Divergent Capitalist

© 2023 LBNN - All rights reserved.