Formal verification

Last updated
Not to be confused with Verificationism.For the Wikipedia policy, see Wikipedia:Verifiability.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. [1] Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.

Contents

Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code in a programming language. Prominent examples of verified software systems include the CompCert verified C compiler and the seL4 high-assurance operating system kernel.

The verification of these systems is done by ensuring the existence of a formal proof of a mathematical model of the system. [2] Examples of mathematical objects used to model systems are: finite-state machines, labelled transition systems, Horn clauses, Petri nets, vector addition systems, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational semantics, axiomatic semantics and Hoare logic. [3]

Approaches

One approach and formation is model checking, which consists of a systematically exhaustive exploration of the mathematical model (this is possible for finite models, but also for some infinite models where infinite sets of states can be effectively represented finitely by using abstraction or taking advantage of symmetry). Usually, this consists of exploring all states and transitions in the model, by using smart and domain-specific abstraction techniques to consider whole groups of states in a single operation and reduce computing time. Implementation techniques include state space enumeration, symbolic state space enumeration, abstract interpretation, symbolic simulation, abstraction refinement.[ citation needed ] The properties to be verified are often described in temporal logics, such as linear temporal logic (LTL), Property Specification Language (PSL), SystemVerilog Assertions (SVA), [4] or computational tree logic (CTL). The great advantage of model checking is that it is often fully automatic; its primary disadvantage is that it does not in general scale to large systems; symbolic models are typically limited to a few hundred bits of state, while explicit state enumeration requires the state space being explored to be relatively small.

Another approach is deductive verification. It consists of generating from the system and its specifications (and possibly other annotations) a collection of mathematical proof obligations, the truth of which imply conformance of the system to its specification, and discharging these obligations using either proof assistants (interactive theorem provers) (such as HOL, ACL2, Isabelle, Coq or PVS), or automatic theorem provers, including in particular satisfiability modulo theories (SMT) solvers. This approach has the disadvantage that it may require the user to understand in detail why the system works correctly, and to convey this information to the verification system, either in the form of a sequence of theorems to be proved or in the form of specifications (invariants, preconditions, postconditions) of system components (e.g. functions or procedures) and perhaps subcomponents (such as loops or data structures).

Software

Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Subareas of formal verification include deductive verification (see above), abstract interpretation, automated theorem proving, type systems, and lightweight formal methods. A promising type-based verification approach is dependently typed programming, in which the types of functions include (at least part of) those functions' specifications, and type-checking the code establishes its correctness against those specifications. Fully featured dependently typed languages support deductive verification as a special case.

Another complementary approach is program derivation, in which efficient code is produced from functional specifications by a series of correctness-preserving steps. An example of this approach is the Bird–Meertens formalism, and this approach can be seen as another form of correctness by construction.

These techniques can be sound , meaning that the verified properties can be logically deduced from the semantics, or unsound, meaning that there is no such guarantee. A sound technique yields a result only once it has covered the entire space of possibilities. An example of an unsound technique is one that covers only a subset of the possibilities, for instance only integers up to a certain number, and give a "good-enough" result. Techniques can also be decidable , meaning that their algorithmic implementations are guaranteed to terminate with an answer, or undecidable, meaning that they may never terminate. By bounding the scope of possibilities, unsound techniques that are decidable might be able to be constructed when no decidable sound techniques are available.

Verification and validation

Verification is one aspect of testing a product's fitness for purpose. Validation is the complementary aspect. Often one refers to the overall checking process as V & V.

The verification process consists of static/structural and dynamic/behavioral aspects. E.g., for a software product one can inspect the source code (static) and run against specific test cases (dynamic). Validation usually can be done only dynamically, i.e., the product is tested by putting it through typical and atypical usages ("Does it satisfactorily meet all use cases?").

Automated program repair

Program repair is performed with respect to an oracle, encompassing the desired functionality of the program which is used for validation of the generated fix. A simple example is a test-suite—the input/output pairs specify the functionality of the program. A variety of techniques are employed, most notably using satisfiability modulo theories (SMT) solvers, and genetic programming, [5] using evolutionary computing to generate and evaluate possible candidates for fixes. The former method is deterministic, while the latter is randomized.

Program repair combines techniques from formal verification and program synthesis. Fault-localization techniques in formal verification are used to compute program points which might be possible bug-locations, which can be targeted by the synthesis modules. Repair systems often focus on a small pre-defined class of bugs in order to reduce the search space. Industrial use is limited owing to the computational cost of existing techniques.

Industry use

The growth in complexity of designs increases the importance of formal verification techniques in the hardware industry. [6] [7] At present, formal verification is used by most or all leading hardware companies, [8] but its use in the software industry is still languishing.[ citation needed ] This could be attributed to the greater need in the hardware industry, where errors have greater commercial significance.[ citation needed ] Because of the potential subtle interactions between components, it is increasingly difficult to exercise a realistic set of possibilities by simulation. Important aspects of hardware design are amenable to automated proof methods, making formal verification easier to introduce and more productive. [9]

As of 2011, several operating systems have been formally verified: NICTA's Secure Embedded L4 microkernel, sold commercially as seL4 by OK Labs; [10] OSEK/VDX based real-time operating system ORIENTAIS by East China Normal University;[ citation needed ] Green Hills Software's Integrity operating system;[ citation needed ] and SYSGO's PikeOS. [11] [12] In 2016, a team led by Zhong Shao at Yale developed a formally verified operating system kernel called CertiKOS. [13] [14]

As of 2017, formal verification has been applied to the design of large computer networks through a mathematical model of the network, [15] and as part of a new network technology category, intent-based networking. [16] Network software vendors that offer formal verification solutions include Cisco [17] Forward Networks [18] [19] and Veriflow Systems. [20]

The SPARK programming language provides a toolset which enables software development with formal verification and is used in several high-integrity systems.[ citation needed ]

The CompCert C compiler is a formally verified C compiler implementing the majority of ISO C. [21] [22]

See also

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

In computer science, static program analysis is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution in the integrated environment.

In computer engineering, a hardware description language (HDL) is a specialized computer language used to describe the structure and behavior of electronic circuits, most commonly to design ASICs and program FPGAs.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

<span class="mw-page-title-main">Isabelle (proof assistant)</span> Higher-order logic (HOL) automated theorem prover

The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.

<span class="mw-page-title-main">ACL2</span> Programming language and theorem prover

ACL2 is a software system consisting of a programming language, an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for software and hardware verification. The input language and implementation of ACL2 are written in Common Lisp. ACL2 is free and open-source software.

Computer science is the study of the theoretical foundations of information and computation and their implementation and application in computer systems. One well known subject classification system for computer science is the ACM Computing Classification System devised by the Association for Computing Machinery.

<span class="mw-page-title-main">Model checking</span> Computer science field

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

In theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified. Best explored is functional correctness, which refers to the input-output behavior of the algorithm.

Software verification is a discipline of software engineering, programming languages, and theory of computation whose goal is to assure that software satisfies the expected requirements.

In software project management, software testing, and software engineering, verification and validation (V&V) is the process of checking that a software system meets specifications and requirements so that it fulfills its intended purpose. It may also be referred to as software quality control. It is normally the responsibility of software testers as part of the software development lifecycle. In simple terms, software verification is: "Assuming we should build X, does our software achieve its goals without any bugs or gaps?" On the other hand, software validation is: "Was X what we should have built? Does X meet the high-level requirements?"

<span class="mw-page-title-main">Logic in computer science</span> Academic discipline

Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas:

In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.

Runtime verification is a computing system analysis and execution approach based on extracting information from a running system and using it to detect and possibly react to observed behaviors satisfying or violating certain properties. Some very particular properties, such as datarace and deadlock freedom, are typically desired to be satisfied by all systems and may be best implemented algorithmically. Other properties can be more conveniently captured as formal specifications. Runtime verification specifications are typically expressed in trace predicate formalisms, such as finite state machines, regular expressions, context-free patterns, linear temporal logics, etc., or extensions of these. This allows for a less ad-hoc approach than normal testing. However, any mechanism for monitoring an executing system is considered runtime verification, including verifying against test oracles and reference implementations. When formal requirements specifications are provided, monitors are synthesized from them and infused within the system by means of instrumentation. Runtime verification can be used for many purposes, such as security or safety policy monitoring, debugging, testing, verification, validation, profiling, fault protection, behavior modification, etc. Runtime verification avoids the complexity of traditional formal verification techniques, such as model checking and theorem proving, by analyzing only one or a few execution traces and by working directly with the actual system, thus scaling up relatively well and giving more confidence in the results of the analysis, at the expense of less coverage. Moreover, through its reflective capabilities runtime verification can be made an integral part of the target system, monitoring and guiding its execution during deployment.

Functional verification is the task of verifying that the logic design conforms to specification. Functional verification attempts to answer the question "Does this proposed design do what is intended?" This is complex and takes the majority of time and effort in most large electronic system design projects. Functional verification is a part of more encompassing design verification, which, besides functional verification, considers non-functional aspects like timing, layout and power.

In computer programming, a programming language specification is a documentation artifact that defines a programming language so that users and implementors can agree on what programs in that language mean. Specifications are typically detailed and formal, and primarily used by implementors, with users referring to them in case of ambiguity; the C++ specification is frequently cited by users, for instance, due to the complexity. Related documentation includes a programming language reference, which is intended expressly for users, and a programming language rationale, which explains why the specification is written as it is; these are typically more informal than a specification.

<span class="mw-page-title-main">Edmund M. Clarke</span> American computer scientist (1945–2020)

Edmund Melson Clarke, Jr. was an American computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs. He was the FORE Systems Professor of Computer Science at Carnegie Mellon University. Clarke, along with E. Allen Emerson and Joseph Sifakis, received the 2007 ACM Turing Award.

In computing, compiler correctness is the branch of computer science that deals with trying to show that a compiler behaves according to its language specification. Techniques include developing the compiler using formal methods and using rigorous testing on an existing compiler.

<span class="mw-page-title-main">Construction and Analysis of Distributed Processes</span>

CADP is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team at INRIA Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.

<span class="mw-page-title-main">Device driver synthesis and verification</span>

Device drivers are programs which allow software or higher-level computer programs to interact with a hardware device. These software components act as a link between the devices and the operating systems, communicating with each of these systems and executing commands. They provide an abstraction layer for the software above and also mediate the communication between the operating system kernel and the devices below.

References

  1. ↑ Sanghavi, Alok (May 21, 2010). "What is formal verification?". EE Times Asia.
  2. ↑ Sanjit A. Seshia; Natasha Sharygina; Stavros Tripakis (2018). "Chapter 3: Modeling for Verification". In Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.). Handbook of Model Checking. Springer. pp. 75–105. doi:10.1007/978-3-319-10575-8. ISBN   978-3-319-10574-1.
  3. ↑ Introduction to Formal Verification, Berkeley University of California, Retrieved November 6, 2013
  4. ↑ Cohen, Ben; Venkataramanan, Srinivasan; Kumari, Ajeetha; Piper, Lisa (2015). SystemVerilog Assertions Handbook (4th ed.). CreateSpace Independent Publishing Platform. ISBN   978-1518681448.
  5. ↑ Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer, Westley (January 2012). "GenProg: A Generic Method for Automatic Software Repair". IEEE Transactions on Software Engineering. 38 (1): 54–72. doi:10.1109/TSE.2011.104. S2CID   4111307.
  6. ↑ Harrison, J. (2003). "Formal verification at Intel". 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. pp. 45–54. doi:10.1109/LICS.2003.1210044. ISBN   978-0-7695-1884-8. S2CID   44585546.
  7. ↑ Formal verification of a real-time hardware design. Portal.acm.org (June 27, 1983). Retrieved on April 30, 2011.
  8. ↑ "Formal Verification: An Essential Tool for Modern VLSI Design by Erik Seligman, Tom Schubert, and M V Achutha Kirankumar". 2015.
  9. ↑ "Formal Verification in Industry" (PDF). Retrieved September 20, 2012.
  10. ↑ "Abstract Formal Specification of the seL4/ARMv6 API" (PDF). Archived from the original (PDF) on May 21, 2015. Retrieved May 19, 2015.
  11. ↑ Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS Archived July 19, 2011, at the Wayback Machine
  12. ↑ "Getting it Right" by Jack Ganssle
  13. ↑ Harris, Robin. "Unhackable OS? CertiKOS enables creation of secure system kernels". ZDNet. Retrieved June 10, 2019.
  14. ↑ "CertiKOS: Yale develops world's first hacker-resistant operating system". International Business Times UK. November 15, 2016. Retrieved June 10, 2019.
  15. ↑ Scroxton, Alex. "For Cisco, intent-based networking heralds future tech demands". Computer Weekly. Retrieved February 12, 2018.
  16. ↑ Lerner, Andrew. "Intent-based networking". Gartner. Retrieved February 12, 2018.
  17. ↑ Kerravala, Zeus. "Cisco brings intent based networks to the data center". NetworkWorld. Archived from the original on December 11, 2023. Retrieved February 12, 2018.
  18. ↑ "Forward Networks: Accelerating and De-risking Network Operations". Insights Success. January 16, 2018. Retrieved February 12, 2018.
  19. ↑ "Getting Grounded in Intent=based Networking" (PDF). NetworkWorld. Retrieved February 12, 2018.
  20. ↑ "Veriflow Systems". Bloomberg. Retrieved February 12, 2018.
  21. ↑ "CompCert - The CompCert C compiler". compcert.org. Retrieved February 22, 2023.
  22. ↑ Barrière, Aurèle; Blazy, Sandrine; Pichardie, David (January 9, 2023). "Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler". Proceedings of the ACM on Programming Languages. 7 (POPL): 249–277. arXiv: 2212.03129 . doi: 10.1145/3571202 . ISSN   2475-1421. S2CID   253736486.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.