Guide to Software Verification with Frama-C: Core Components, Usages, and Applications (Computer Science Foundations and Applied Logic)

Foreword
Preface
Acknowledgements
List of Reviewers
Contents
Contributors
Part I Core Components and Analyzers
1 Formally Expressing What a Program Should Do: The ACSL Language
	1.1 On Formal Specification Languages
	1.2 Function Contracts
		1.2.1 Basic Function Contracts
		1.2.2 Additional Constructs and Syntactic Sugar for Contracts
		1.2.3 Towards a Formal Semantics of Contracts
		1.2.4 Specifying Side Effects: Framing and Referring to Former Values
		1.2.5 Contracts with Multiple Cases: Behaviors
	1.3 The Core Logic of ACSL
		1.3.1 Terms and Formulas in ACSL
		1.3.2 Built-In Logic Theories of ACSL
		1.3.3 Semantics of Propositions
		1.3.4 Total Functions and Underspecified Terms
	1.4 Code Annotations
		1.4.1 Code Assertions
		1.4.2 Referring to the Past Using Labels
		1.4.3 Formalizing Semantics of Assertions and Labels
		1.4.4 Loop Annotations
		1.4.5 Loop Invariants in Presence of break and continue Statements
		1.4.6 Formal Semantics of Loop Invariants
		1.4.7 Specifying Termination
	1.5 Describing Memory
		1.5.1 Structure of Memory Blocks
		1.5.2 Validity of Memory Locations
		1.5.3 Specifying Memory Separation
	1.6 Ghost Code
		1.6.1 Ghost Memory
		1.6.2 Interaction with Control Flow
		1.6.3 Ghost Code Annotations
	1.7 Global Annotations
		1.7.1 Defining Predicates and Functions
		1.7.2 Referring to Memory States
		1.7.3 Inductive Predicates
		1.7.4 Axiomatics
		1.7.5 The Danger of Inconsistent Axiomatizations
	1.8 Conclusion
	1.9  Answers to Exercises
	References
2 The Heart of Frama-C: The Frama-C Kernel
	2.1 Running Frama-C
		2.1.1 Invoking Frama-C
		2.1.2 Brief Overview of Frama-C\'s Command Line
	2.2 Plug-ins
		2.2.1 Plug-in Collaboration
		2.2.2 Plug-in Gallery
		2.2.3 Expressiveness Plug-ins
		2.2.4 Support Plug-ins
		2.2.5 ``Understanding\'\' Plug-ins
		2.2.6 Loading Plug-ins
	2.3 Parsing Annotated C code
		2.3.1 Preprocessing C and Build Tools
		2.3.2 From Preprocessed Code to Typed and Unified AST
		2.3.3 Kernel and Plug-in Transformations and Cleanup
		2.3.4 Supporting Several C Standards, and Non-Standard Extensions
		2.3.5 Standard C Library, a.k.a. libc, and POSIX
		2.3.6 Architecture-Dependent Features: Frama-C\'s machdep
		2.3.7 ACSL: a Lingua Franca, But Not Equally Well-Spoken
	2.4 Normalized Code Representation
		2.4.1 Side Effects and Sequencing
		2.4.2 Making Implicit Conversions Explicit
		2.4.3 Logical Operators
		2.4.4 Loops
		2.4.5 Return Statement
		2.4.6 Assembly Code
	2.5 Driving Frama-C
		2.5.1 Handling Frama-C Warnings
		2.5.2 Sequencing Analyses
		2.5.3 Saving to and Loading from Disk Previous Results
	2.6 Visualizing Analyses Results
		2.6.1 Property Statuses
		2.6.2 Generating Reports
	2.7 Conclusion
	References
3 Abstract Interpretation with the Eva Plug-in
	3.1 Introduction
		3.1.1 Main Features
		3.1.2 First Example
		3.1.3 Overview
	3.2 Abstract Interpretation
		3.2.1 Experiment with Eva
		3.2.2 Soundness
		3.2.3 Algorithm Termination
	3.3 Abstract Domains in Eva
		3.3.1 Abstractions of C Values
		3.3.2 The Cvalue Domain
		3.3.3 Symbolic Domains
		3.3.4 Relational Domains
		3.3.5 Inferring New Properties
		3.3.6 Communication Between Abstract Domains
	3.4 State Partitioning
		3.4.1 Experiment with State Partitioning
		3.4.2 Theory
		3.4.3 Loop Unrolling
		3.4.4 Case-Based Reasoning
		3.4.5 Path-Based Reasoning
		3.4.6 Brute-Force Partitioning
	3.5 Setting Up an Analysis
		3.5.1 Code Availability, Stubs, Specifications, Builtins
		3.5.2 Main Function
		3.5.3 Iterative Refinement
	3.6 Results of an Eva Analysis
		3.6.1 Undesirable Behaviors Detected by Eva
		3.6.2 libc Pre-conditions
		3.6.3 User Assertions
		3.6.4 Graphical Interface
		3.6.5 API
		3.6.6 Limitations
	3.7 Conclusion
	References
4 Formally Verifying that a Program Does What It Should: The Wp Plug-in
	4.1 Introduction
	4.2 Deductive Verification of Programs
		4.2.1 Companion Provers
		4.2.2 An Example Program
		4.2.3 Handling Runtime Errors
		4.2.4 Fixing the Example Program
		4.2.5 Combining Wp with Other Plug-ins
	4.3 Memory Models and Related Properties
		4.3.1 Simple Variable Assignments
		4.3.2 Introducing Pointers
		4.3.3 The General WP Memory Model
		4.3.4 The Typed Memory Model
		4.3.5 Mixing Aliasing and Non-aliasing
		4.3.6 Base-Pointer Memory Regions
		4.3.7 Pointers as References
		4.3.8 Memory Allocation
		4.3.9 Initialization
	4.4 Annotations
		4.4.1 Assertions
		4.4.2 Function Calls
		4.4.3 Loop Invariants
		4.4.4 Writing Loop Annotations
		4.4.5 Termination
		4.4.6 Lemmas and Axiomatic Definitions
		4.4.7 Ghost Code and Lemma Functions
		4.4.8 Proving Generated Annotations
		4.4.9 Annotations and Verification Conditions
	4.5 Detecting Specification Errors
		4.5.1 Specification Threats
		4.5.2 Testing the Specifications
	4.6 Sequent Simplification and Interactive Proof
		4.6.1 Normalization and Term Simplifications
		4.6.2 Sequent Decomposition
		4.6.3 Sequent Simplifications
		4.6.4 The Interactive Prover (TIP)
		4.6.5 Using External Proof Assistants
	4.7 Related Work
		4.7.1 Hoare Logic
		4.7.2 Separation Logic
		4.7.3 Deep Embedding
		4.7.4 C-Extraction
		4.7.5 Model Checking
		4.7.6 Choose Your Tool
	4.8 Conclusion
	References
5 Runtime Annotation Checking with Frama-C: The E-ACSL Plug-in
	5.1 Runtime Annotation Checking
	5.2 An Executable Subset of ACSL
		5.2.1 Expressiveness of the E-ACSL Language
		5.2.2 Semantics of the E-ACSL Language
	5.3 How to Use E-ACSL Plug-In
		5.3.1 What is E-ACSL, Basic Usage
		5.3.2 Checking Undefined Behaviors
		5.3.3 Checking Other Properties
	5.4 Effective Usage of E-ACSL Plug-in
		5.4.1 Fine-Tuning E-ACSL
		5.4.2 Guarantees Offered by E-ACSL and Comparison with Other Tools
		5.4.3 How to Integrate E-ACSL in Software Development Life Cycle
	5.5 Design and Technical Solutions for E-ACSL
		5.5.1 Software Architecture
		5.5.2 Arithmetic Properties
		5.5.3 Memory Properties
	5.6 Conclusion and Perspectives
	References
6 Test Generation with PathCrawler
	6.1 Introduction
	6.2 Structural Testing
	6.3 PathCrawler: What it Does
	6.4 PathCrawler: How it Works
	6.5 Using PathCrawler in Practice
		6.5.1 Stubbing
		6.5.2 Constant Inputs
		6.5.3 Precondition
		6.5.4 Coverage Options
		6.5.5 Oracle
		6.5.6 Testing Faulty Code
	6.6 PathCrawler-online
		6.6.1 Inputs of PathCrawler-online
		6.6.2 Ouputs of PathCrawler-online
		6.6.3 Benefits and Limitations
	6.7 The Place of Structural Testing in the Verification and Validation Process
	6.8 Conclusion
	References
Part II Advanced Usages and Analyses
7 The Art of Developing Frama-C Plug-ins
	7.1 Running Example
		7.1.1 Typestates
		7.1.2 Requirements for MiniTypeState
	7.2 Plug-in Setup
	7.3 Plug-in Inputs/Outputs
		7.3.1 Entry Point
		7.3.2 Basic Debugging and Pretty-Printing
		7.3.3 Outputting Messages
		7.3.4 Command-Line Options
	7.4 AST and Associated Tables
		7.4.1 Accessing the Complete AST
		7.4.2 Accessing a Specific Node
		7.4.3 AST Transformations
		7.4.4 Using the Control-Flow Graph
		7.4.5 Accessing ACSL Annotations
	7.5 Datatype and Project Libraries
		7.5.1 Datatype Library
		7.5.2 Project Library
	7.6 Visitor
		7.6.1 Overview of the Visitor Mechanism in Frama-C
		7.6.2 Observing the AST with an Inplace Visitor
		7.6.3 Creating a Code Transformation Pass with an Inplace Visitor
		7.6.4 Creating a New AST with a Copy Visitor
	7.7 Interpreted Automata
		7.7.1 Automaton Description
		7.7.2 Using an Automaton to Implement a Dataflow Analysis
	7.8 Plug-in Packaging
		7.8.1 Testing
		7.8.2 Distribution
	7.9 Conclusion
	References
8 Tools for Program Understanding
	8.1 Introduction
	8.2 Ivette: A New Graphical Interface
	8.3 Metrics
	8.4 Studia
	8.5 Dive
	8.6 Analysis Scripts
		8.6.1 Motivating Example
		8.6.2 Heuristics-Based Scripts
		8.6.3 Configuring and Building
		8.6.4 Analysis Template
		8.6.5 Miscellaneous Utilities
		8.6.6 Conclusion
	References
9 Combining Analyses Within Frama-C
	9.1 Introduction
	9.2 Combinations of Model Checking with Frama-C Analyzers
		9.2.1 The CEGAR Approach
		9.2.2 CegarMC Architecture
		9.2.3 Exploiting Value Analysis
		9.2.4 Integrating Deductive Verification
	9.3 Lightening Static Analyses by Means of Runtime Verification
		9.3.1 Verifying ACSL Annotations with E-ACSL
		9.3.2 Combining Runtime Verification with Value Analysis
		9.3.3 Combining Runtime Verification with Deductive Verification
		9.3.4 Beyond ACSL Properties
	9.4 Combinations of Static Analysis with Test Generation
		9.4.1 Test Generation to Classify Alarms Produced by Value Analysis
		9.4.2 Test Generation to Diagnose Proof Failures
		9.4.3 Detecting Infeasible Test Objectives by Static Analysis
	9.5 Points of Attention for Integrative Techniques
	9.6 Conclusion
	References
10 Specification and Verification  of High-Level Properties
	10.1 Introduction
	10.2 Pervasive Program Properties
		10.2.1 Illustrative Examples of Properties
		10.2.2 The MetAcsl Plug-In
	10.3 Verification of Pervasive Properties with MetAcsl
	10.4 Relational Properties
		10.4.1 Example of Relational Property
		10.4.2 Specification of Relational Properties in RPP
	10.5 Verification of Relational Properties with RPP
		10.5.1 Code Transformation
		10.5.2 Back to the Illustrative Example
	10.6 Properties Over Call Traces
		10.6.1 Informal Properties
		10.6.2 Automaton
		10.6.3 The Aoraï Plug-In
		10.6.4 The Ya Language
	10.7 Verification of Properties Over Call Traces with Aoraï
		10.7.1 Code Instrumentation by Aoraï
		10.7.2 Analysis of the Instrumented Code with Wp
		10.7.3 Analysis of the Instrumented Code with Eva
	10.8 Conclusion
	References
11 Advanced Memory and Shape Analyses
	11.1 Introduction
	11.2 Overview
		11.2.1 Motivating Example
		11.2.2 Type-Based Shape Analysis
		11.2.3 Separation Logic and  Relational Separation-Logic-Based Analysis
		11.2.4 Discussion
	11.3 Abstract Interpretation Framework
		11.3.1 Program States and Concrete Execution
		11.3.2 Sound Static Analyses by Abstract Interpretation
		11.3.3 Base Abstractions
	11.4 Type-Based Static Analysis with the Codex Plug-in
		11.4.1 Well-Typed States
		11.4.2 The Type Abstraction
		11.4.3 Points-to Predicates
	11.5 Separation-Logic-Based Analysis with the  RMA Plug-In
		11.5.1 Abstract Heaps and State Analysis
		11.5.2 Abstract Heap Transformations and  Transformation Analysis
	11.6 Further Reading
	11.7 Conclusion
	References
12 Analysis of Embedded Numerical Programs in the Presence of Numerical Filters
	12.1 Introduction
	12.2 Problematic Aspects of Linear Digital Filters
	12.3 Analysis of a Filter of Order 1 with Frama-C
	12.4 Analysis of a Filter of Order 2 Having Real Eigenvalues
	12.5 Analysis of a Filter of Order 2 Having Complex Eigenvalues
		12.5.1 Invariant as a Set of Intervals
		12.5.2 Optimal Invariant with Linear Algebra
		12.5.3 Invariant as an Ellipsoid
		12.5.4 Invariant as a Zonotope
	12.6 Conclusion
	References
Part III Case Studies and Industrial Applications
13 An Exercise in Mind Reading: Automatic Contract Inference for Frama-C
	13.1 Introduction
	13.2 Preliminaries
		13.2.1 Hoare Logic and Contract-Based Verification
		13.2.2 Target Programming Language and Semantics
		13.2.3 Constrained Horn Clauses (CHCs)
		13.2.4 CHC-Based Model-Checking
		13.2.5 The TriCera Model Checker
	13.3 Contract Inference Using Assertion-Based Model Checking
		13.3.1 The Harness Function
		13.3.2 Inferring Contracts with TriCera
	13.4 The Saida Plugin
		13.4.1 Generating the Harness Function
		13.4.2 Inferring Contracts
		13.4.3 Using Inferred Contracts for Verification
		13.4.4 Handling Recursive Functions
		13.4.5 Limitations
	13.5 Extensions and Ongoing Work
		13.5.1 Programs with Loops
		13.5.2 Programs with Pointers and Heap Allocations
		13.5.3 Inferring assigns Clauses
		13.5.4 Inferring Partial Contracts
		13.5.5 Contracts with Uninterpreted Predicates
		13.5.6 Inferring Contracts for Library/API Functions
	13.6 Conclusion
	References
14 Exploring Frama-C Resources by Verifying Space Software
	14.1 Is Static Analysis Worthwhile?
	14.2 Literature Review of Frama-C Applications
	14.3 Overview of IAE Satellite Launcher Projects
		14.3.1 Case Study: Embedded Aerospace INS Software
	14.4 Employing Frama-C in Space Software
		14.4.1 Former Experiment: Embedded Aerospace Control Software
		14.4.2 Current Experiment: Embedded Aerospace INS Software
		14.4.3 SSISNAV Analysis with the Callgraph Plug-In
		14.4.4 SSISNAV Analysis with the SpareCode Plug-In
		14.4.5 SSISNAV Analysis with the Metrics Plug-In
		14.4.6 SSISNAV Analysis with the Eva Plug-In
		14.4.7 Reporting of Anomalies Found in the Analyses
	14.5 Conclusion
	References
15 Ten Years of Industrial Experiments with Frama-C at Mitsubishi Electric R&D Centre Europe
	15.1 Introduction
	15.2 Industrial Code Verification with Eva
		15.2.1 Organizing People for Verification
		15.2.2 Method for Safety-Critical Code Verification
		15.2.3 Practical Configuration of Eva
		15.2.4 Challenges of Analyzing Big Source Code
		15.2.5 Tips and Tricks to Improve Eva Analysis Precision
		15.2.6 Conclusion
	15.3 Automated Test Generation Using Eva and PathCrawler
		15.3.1 Technological Context
		15.3.2 Tool Architecture
		15.3.3 Generation of Test Objectives for Different Back-End Tools
		15.3.4 Generation of Stubs
		15.3.5 Results
		15.3.6 Related Work
		15.3.7 Conclusion and Future Work
	15.4 Verifying That a Firewall Is Correctly Configured with Frama-C
		15.4.1 Modeling and Verification Using Simulink
		15.4.2 Simulating and Verifying the Model
		15.4.3 Generating the Monitor
		15.4.4 Discussion
	15.5 Conclusion
	References
16 Proof of Security Properties: Application to JavaCard Virtual Machine
	16.1 Introduction
	16.2 General Presentation of the JavaCard Virtual Machine
	16.3 Overview of the Secure Policy Model
		16.3.1 Code and Heap Modeling
		16.3.2 Examples of Functions
	16.4 Security Properties: Predicates and Metaproperties
	16.5 Proof Results
	16.6 Summary of Lessons Learned and Challenges
	16.7 Future Enhancements
	References
Appendix  Index
Index