What is high-assurance software, and what are its benefits?
Many of the systems that are important to national security undergo rigorous certification and evaluation regimes. Yet they remain vulnerable to hackers and attackers, don’t work as they are supposed to, or stop working altogether due to errors that evaluation and certification alone fail to discover.
The most critical software and hardware systems (like those that control nuclear reactors, rockets, and unmanned aerial vehicles) go beyond evaluation and certification to provide guarantees and mathematical evidence that they will function exactly as intended at all times. These systems also require guarantees that they are not susceptible to conventional hacking attempts, which have become a common occurrence. The makers of these systems use tools and techniques that produce high-assurance software: software that is mathematically proven to function as intended, and only as intended.
Like software that controls a nuclear reactor, elections software should be guaranteed to work only as intended, and provide clear and compelling evidence that it does so, going beyond conventional evaluation.
High-assurance systems are built in such a way that it is possible to prove with mathematical certainty that they work precisely as intended and as designed. These systems provide clear, digital evidence that can be checked by third parties to prove that they work exactly as intended—no more, no less.
We have produced high-assurance software and systems critical to national security for more than a decade, and along the way we have built a team of computer scientists who are on the cutting edge of software verification and cryptography. We are excited to bring the robustness of high-assurance software to the elections world.
High-assurance software engineering vs. conventional software engineering
Very few organizations can build high-assurance software. High-assurance techniques have been used for decades to produce critical chips and software, mostly for national security purposes. However, they have only recently become powerful and affordable enough to produce large pieces of software like election systems. High-assurance software engineering still requires computer scientists on the cutting edge of software verification, and is rarely seen outside critical systems.
Conventional software engineering does not provide the evidence and guarantees required for high assurance. Testing and evaluation are often enough for deploying conventional software systems, even though it is widely accepted that they can only cover a subset of potential issues and problems. When conventional software crashes, glitches, or malfunctions, it restarts, loses data, or stops working until fixed. Since most systems do not control critical infrastructure, this is considered acceptable behavior. That is why most people’s experiences with software include crashes, malfunctions, and even data loss.
Conventional software systems work well enough and have powered the rise of new technologies, apps, and platforms that are changing the world. However, very few conventional software systems require absolute guarantees that they will not malfunction. High-assurance systems, on the other hand, are deployed in places like financial institutions, aircraft, and defense systems, where failure is unacceptable.
High-assurance democracy
Traditionally, the rigorous processes that produce high-assurance software have been applied only to systems critical to infrastructure and national security. We strongly believe that democracy should be treated as a critical system, and that voting should be conducted using high-assurance systems. Free & Fair systems offer the benefits and trustworthiness of high-assurance systems along with the cost benefits of a transparent B corporation whose mission is to make elections more trustworthy and affordable for all.