Improving system verification

When end users open a program on their computer, they expect it to function properly without any hiccups. But ensuring that systems perform correctly is more complex than you may think. With hundreds of thousands of lines of code, just one programming error can introduce a myriad of potential issues.

Using a technique called formal verification provides high assurance by eliminating certain classes of bugs. However, to use it, developers need to spend countless hours writing proofs that demonstrate their code’s correctness to a mechanical proof checker. Historically, this has been a slow and daunting task, but now researchers at Carnegie Mellon have developed a unique method to help speed up the process and improve developer efficiency.

In their new paper, “Linear Types for Large-Scale Systems Verification,” which won an ACM SIGPLAN Distinguished Paper Award at this year’s Object-oriented Programming Systems, Languages, and Applications (OOPSLA) Conference, Bryan Parno, associate professor in CMU’s Electrical and Computer Engineering (ECE) and Computer Science (CSD) departments, and Yi Zhou, a Ph.D. student in CSD, along with fellow researchers from academia and industry, present a hybrid approach that combines linear types with SMT-based verification for memory reasoning. 

“System verification is one of the main areas our research group focuses on,” says Zhou. “We look to prove properties about existing systems, ensuring they perform as intended by creating machine-checkable proofs that provide high assurance of security and reliability.”

Aliasing is a common feature in programming languages that allows the same data location to be accessed through different variable names. Modification to a variable also indirectly changes the value associated with all aliased variables.

However, aliasing is difficult for both developers and machine-based proof checkers to reason about. Proving that aliasing is managed correctly often requires the developer to spell out their reasoning in tedious detail. And even then, proof checkers can become ‘confused’, slowing the verification process with little to no feedback as to why.

“The checker might fail to prove a statement but have a hard time giving any specific reasons,” says Zhou. “Sometimes it simply gets stuck for a long time.”

To address this problem, researchers made a key observation: while aliasing could happen between any pair of variables, in reality, it rarely does. Based on this insight, the group developed a method that draws on a form of reasoning called “linear logic,” which efficiently handles the common case. The study’s authors also demonstrate how to make linear logic compatible with existing reasoning techniques to handle those rare instances in which reasoning about aliasing is still needed.

“Our method not only improves the efficiency of machine verification, it also gives developers an easier and more pleasant experience.”

Paper Reference

Linear Types for Large-Scale Systems Verification

• Jialin Li, University of Washington
• Andrea Lattuada, ETH Zurich
• Yi Zhou, Carnegie Mellon University
  Computer Science Department
• Jonathan Cameron, Carnegie Mellon University
  Computer Science Department
• Jon Howell, VMware Research, USA
• Bryan Parno, Carnegie Mellon University
  Electrical and Computer Science and Computer Science Departments
• Chris Hawblitzel, Microsoft Research

This study was presented at ACM SIGPLAN’s Object-oriented Programming Systems, Languages, and Applications (OOPSLA) Conference and is available here.