Skip to main content
PRL Project

On Hardening

The term "hardening" is meant to evoke the processes by which a metal is made stronger or a command center is made impervious to attack. We imagine an incremental process that can produce various degrees of strength depending on requirements.

In the case of software, we have in mind that more and more properties of the system are specified formally. Some properties can be checked by type checkers, or extended type checkers, or by model checkers. Some are examined by decision procedures. Some of the arguments given by the designers and programmers to convince people that the code has various properties are made more precise. Some of the arguments will be written and checked by other people. Some will become proofs; some will become rigorous proofs; some will become semi-formal proofs with steps justified by referring to well known facts; some will become formal proofs with every step checked; and some will become completely formal proofs done in foundational provers; and some will become completely formal proofs in foundational provers that have been hardened and whose primitive proofs are checked by multiple checkers on multiple platforms.

These steps are progressively more stringent, leading to harder code; presently the steps are progressively more costly as well. But even the highest of these standards does not provide absolute certainty. There is no such thing in the physical world whose fundamental laws are probabilistic. We can only reduce the probability of error and create software that is hardened enough for its task.

Just as with materials, there is always a use for stronger ones. The ability to harden software is also the ability to do more with software systems.