What Is Software Correctness?
We rely on software to control almost everything around us. Interaction with embedded systems such as cars, pacemakers, and satellites is part of everyday life. Runtime errors within these systems create liabilities. Preventing these cases before they impact people’s lives is critical. This leaves engineers with the major challenge of demonstrating software correctness.
What is correctness?
A program is correct when it behaves exactly as intended, and no other way. A minimum prerequisite to reach correctness is safety. Engineers should not trust their own code or let others think it is trustworthy without evidence. For software to be considered correct, an engineer must demonstrate that their program works as intended, matching specifications. There are several tools that can help an engineer demonstrate the correctness of their code.
Tools for correctness
The first way an engineer can ensure software correctness is through Deep Specification. DeepSpec establishes the attributes of a comprehensive (deep) specification. In order for a specification to be deep, it must be:
- Rich: Describes complex component behavior in detail
- Live: Connected to the implementation
- Formal: Written in a language with clear semantics that can be consumed by provers and testing tools
- Two-sided: Connected to both implementations and clients
Two common types of tools to create and reason about Deep Specification are interactive proof assistants and property-based testing.
Interactive proof assistants help engineers develop formal proofs about their code. Engineers can use tools like Coq to develop code, write and verify proofs about the code, and then extract the verified code. An engineer has evidence their program behaves as intended when proofs about the code are machine-checked.
Check out this content from our parent company, Galois, on Formal Verification
Property-based testing shows that specification is met over many computer-generated inputs. First, software engineers develop test harnesses in their native software stack. Test harnesses include:
- Description of data to be generated
- Software to test
- Specification written in the native language as boolean expression
Engineers use property-based testing tools like DeepState and Hypothesis to create test harnesses and generate inputs. Property-based testing tools can reveal if program outputs are true to specification.
On their own, property-based testing tools can’t provide evidence at the level of interactive proof assistants. Pairing them with instrumentation such as ASan and UBSan can build confidence in correctness.
What’s the risk?
It’s important to consider risk when reasoning about software correctness. The soundness of tools used to check correctness and program transformations (such as compilation), is important to consider. Property-based testing cannot guarantee specifications will be met, but interactive proof assistants can. If a proof is machine-checked, then the result should be considered correct. The tradeoff is the ease of use of property-based testing tools versus confidence of correctness with interactive proof assistants. Software engineers can execute test harnesses and type check proofs to ensure confidence about the correctness of their software.
Correctness is possible
It is possible to have and demonstrate confidence in software correctness. Writing deep specification for your software and verifying or testing it is the key.
Tangram Flex is a software company in Dayton, Ohio. Our team is a group of leaders from the DoD, private industry, and innovative startups committed to helping engineers build configurable systems for secure, rapid delivery of technology to the market. Have questions? Get in touch with our team.
