Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification
This program is tentative and subject to change.
Memory safety defects pose a major threat to software reliability, enabling cyberattacks, outages, and crashes. To mitigate these risks, organizations adopt Compositional Bounded Model Checking (BMC), using unit proofs to formally verify memory safety. However, methods for creating unit proofs vary across organizations and are inconsistent within the same project, leading to errors and missed defects. In addition, unit proofing remains understudied, with no systematic development methods or empirical evaluations.
This work presents the first empirical study on unit proofing for memory safety verification. We introduce a systematic method for creating unit proofs that leverages verification feedback and objective criteria. Using this approach, we develop 73 unit proofs for four embedded operating systems and evaluate their effectiveness, characteristics, cost, and generalizability. Our results show unit proofs are cost-effective, detecting 74% of recreated defects, with an additional 9% found with increased BMC bounds, and 19 new defects exposed.
We also found that embedded software requires small unit proofs, which can be developed in 87 minutes and executed in 61 minutes on average. These findings provide practical guidance for engineers and empirical data to inform tooling design.
This program is tentative and subject to change.
Fri 17 AprDisplayed time zone: Brasilia, Distrito Federal, Brazil change
11:00 - 12:30 | Dependability and Security 9Research Track / Demonstrations / SE In Practice (SEIP) at Oceania VII Chair(s): Jieke Shi Singapore Management University | ||
11:00 15mTalk | Prophecy: Inferring Formal Properties from Neuron Activations Demonstrations Divya Gopinath KBR; NASA Ames, Corina S. Păsăreanu Carnegie Mellon University, Muhammad Usman University of Texas at Austin, USA Media Attached File Attached | ||
11:15 15mTalk | Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification Research Track Paschal Amusuo Purdue University, Owen Cochell Michigan State University, Taylor Le Lievre Purdue University, Parth Vinod Patil Purdue University, Aravind Machiry Purdue University, James C. Davis Purdue University Pre-print | ||
11:30 15mTalk | Accurate Inference of Termination ConditionsDistinguished Paper Award Research Track | ||
11:45 15mTalk | Verification of Multi-Model Stochastic Systems Research Track Radu Calinescu University of York, UK, Simos Gerasimou Cyprus University of Technology, Sinem Getir Yaman University of York, UK, Gricel Vázquez University of York, UK, Micah Bassett University of York, UK Pre-print | ||
12:00 15mTalk | Accelerating IC3 Verification by Exploiting Unsatisfiable Cores and Satisfying ModelsDistinguished Paper Award Research Track Xinyi Gong National University of Defense Technology, Liangze Yin National University of Defense Technology, Yuhan Li National University of Defense Technology, Ke Kang National University of Defense Technology, Wei Dong National University of Defense Technology, Shanshan Li National University of Defense Technology, Ji Wang National University of Defense Technology | ||
12:15 15mTalk | Agentic Taxation Optimization via LLM SMT-Constraint Reasoning SE In Practice (SEIP) Ting Chien Hwang National Chengchi University, Fang Yu National Chengchi University, Jie-Hong Roland Jiang National Taiwan University | ||