MID-089: Formal Methods Verification of Critical Functionality Implementation
Mitigation Level: Leading
Description
In general, formal verification is the process of proving, typically with an aid of automated or semi-automated tooling, that a particular code module or function satisfies the desired requirements. Depending on the size and complexity of the code to be verified, formal verification can be a time-consuming effort requiring significant expertise. In general, it is significantly easier to verify code that was explicitly designed with formal verification in mind.
Formal verification is capable of eliminating broad classes of software bugs and vulnerabilities, providing otherwise-unprecedented levels of certainty in software correctness and security. By forcing the software designers to consider implications of their design decisions, the use of formal methods often leads to “cleaner” more maintainable designs. In attempting to prove that a property holds, formal verification forces developers to confront and fix all the reasons the property might be violated early in software development process, eliminating costly rework that would have been needed should the errors were left undetected much further into the system development timeline.
A general approach to considering formal verification for a particular system may be outlined as follows. First, what are the most critical functions in the system that are particularly important to implement correctly in order to achieve the desired system-level goals? Note that this may include both the functions directly producing the end-goal functionality for the system, the protection mechanisms for end-goal functionality, or something else. Second, are there existing formally verified implementations (see MID-087) or tools (see MID-088) for that functionality that can be leveraged? If not, what is the formal tooling that may be necessary for establishing the desired properties of the implementations – model-based code synthesis tools, model checkers, interactive theorem provers, or something else? From there, the process often becomes use-case specific, necessitating inputs from domain experts and formal verification experts to choose the right path forward.
Consideration: A strong design will often combine a formally verified microkernel (see MID-087), isolating critical functionality into separate partitions, making sure the code in those partitions is itself formally verified as discussed above, and then ensuring cross-partition and external communication channels are filtered by formally verified parsers (see MID-088).
Limitations: Only properties that were scoped into the formal specification, verification, and/or generator can be guaranteed to carry through into the resulting implementation. Users need to make sure their specifications are complete enough and specific enough to exclude all undesired behaviors. Additionally, users should be aware of the assumptions made in the definition of the specification as any violations of those assumptions would invalidate the proofs and make any conclusions made by the formal verification inapplicable.
IEC 62443 4-2 Mappings
- None
References
[1] Aijaz Fatima. “Introduction to Formal Verification”. May, 2019. [online] Accessed: Apr 15, 2025. Available: https://www.eeweb.com/introduction-to-formal-verification/
[2] K. Fisher, J. Launchbury, R. Richards. “The HACMS program: Using formal methods to eliminate exploitable bugs.” royalsocietypublishing.org. Accessed: Mar. 18, 2025. Available: https://royalsocietypublishing.org/doi/10.1098/rsta.2015.0401
[3] Courtney Albon “DARPA touts ‘formal methods’ for nipping cyber disasters in the bud”. Defense News, Feb 21, 2025. [online] Accessed: Apr 15, 2025. Available: https://www.defensenews.com/pentagon/2025/02/21/darpa-touts-formal-methods-for-nipping-cyber-disasters-in-the-bud/