by COLLINS AEROSPACE
In the contemporary landscape, computing systems often control critical infrastructure, exposing them to risks of cyber-attacks that can compromise security and disrupt functionality. It is imperative to construct these systems with robust guarantees of resiliency against cyber-threats.
Formal verification emerges as a key approach to achieve such assurance, offering proof of system compliance with desired correctness properties that guard the systems against unforeseen errors and/or attacks. The aim of REWIRE is ensure the security and resiliency of systems during their entire life cycle. Thus, in REWIRE we argue that the consideration of security mechanisms that protect systems during their runtime operation is not sufficient, especially in the paradigm of resource constraint and embedded devices where the applicability of runtime protection solution can be limited. Thus, formal verification is the main pillar in REWIRE for synthesizing a complete security-by-design approach which takes place from the design-time phase of systems. REWIRE will use and combine complementary methods to perform verification, among which Model Checking and Theorem Proving.
Model Checking is a method for assessing whether a formal model of a system satisfies a given property, expressed in a formal language; it has the advantage of being fully automated, and it is guaranteed to fully explore the behavior of the system and either prove the validity of the property, or generate evidence of falsification, that helps determine why the property does not hold. Its main drawback, scalability in presence of advanced systems, where the complexity grows exponentially in parameters and components, has substantially improved through the years, thanks to the development of symbolic encodings and algorithms, based on efficient data structures and logic.
Theorem Proving can in principle handle larger systems and more types of properties than model checking can; however, it is a partially automated method and requires user guidance in non-trivial cases, by means of proof assistant software. Properties are represented as goals to be proven and are typically expressed in some form of logic. It should be noted that if the properties refer to particular aspects of a model, these need to be modeled as well in the language of the Theorem prover. After encoding a property as a goal, if this is simple enough, the tool can prove it automatically. Otherwise, the user is responsible for decomposing the goal into subgoals; these can be trivial or not, in which case they may need to be broken down into further subgoals, until everything can, eventually, be verified by the tool. Combination of the partial results (i.e., that each goal is implied by its subgoals) into a global proof is usually performed automatically by the Theorem prover.
REWIRE combines Model Checking and Theorem Proving for ensuring the correctness of critical functions that support the entire systems lifecycle management. Particular focus is given on the correctness of mechanisms offering confidential and authenticated software updates distribution, as well as on operational correctness of cryptographic primitives in the context of RISC-V instruction sets. REWIRE develops a complete verification and validation framework used at design time for capturing overarching requirements to different levels of implementation-abstractions, linking the verification outcomes to constraint run-time security operations. REWIRE team has built the formal verification pipeline and toolchain and more results are about to be published…. Stay tuned!