Amtoft / Browning / Davis Design and Verification of Microprocessor Systems for High-Assurance Applications

1. Auflage 2010
ISBN: 978-1-4419-1539-9
Verlag: Springer-Verlag
Format: PDF
Kopierschutz: Adobe DRM (»Systemvoraussetzungen)

E-Book, Englisch, 436 Seiten

Microprocessors increasingly control and monitor our most critical systems, including automobiles, airliners, medical systems, transportation grids, and defense systems. The relentless march of semiconductor process technology has given engineers exponentially increasing transistor budgets at constant recurring cost. This has encouraged increased functional integration onto a single die, as well as increased architectural sophistication of the functional units themselves. Additionally, design cycle times are decreasing, thus putting increased schedule pressure on engineers. Not surprisingly, this environment has led to a number of uncaught design flaws. Traditional simulation-based design verification has not kept up with the scale or pace of modern microprocessor system design. Formal verification methods offer the promise of improved bug-finding capability, as well as the ability to establish functional correctness of a detailed design relative to a high-level specification. However, widespread use of formal methods has had to await breakthroughs in automated reasoning, integration with engineering design languages and processes, scalability, and usability. This book presents several breakthrough design and verification techniques that allow these powerful formal methods to be employed in the real world of high-assurance microprocessor system design.

Autoren/Hrsg.

Amtoft, Torben

Browning, Selly

Davis, Jared

Inhaltsverzeichnis

1;Preface;6
2;Contents;9
3;ACL2 and Its Applications to Digital System Verification;13
3.1;1 Introduction;13
3.2;2 Some Basic Decisions;13
3.3;3 ACL2;15
3.3.1;3.1 A Programming Language;16
3.3.2;3.2 A Logical Theory;18
3.3.3;3.3 A Mechanical Theorem Prover and Proof Environment;20
3.3.4;3.4 Efficiency;22
3.4;4 A Simple Microprocessor Model;23
3.5;5 Variations on the Theme;29
3.6;6 Summary;30
3.7;References;31
4;A Mechanically Verified Commercial SRT Divider;34
4.1;1 Introduction;34
4.2;2 SRT Division;37
4.3;3 Quotient Digit Selection;42
4.4;4 Implementation;47
4.4.1;4.1 Analysis of Operands;48
4.4.2;4.2 Iteration;52
4.4.3;4.3 Final Computation;58
4.5;References;64
5;Use of Formal Verification at Centaur Technology;75
5.1;1 Introduction;75
5.1.1;1.1 Overview of Verification Methodology;75
5.1.2;1.2 Timeline;76
5.1.3;1.3 Centaur Media Unit;78
5.2;2 Modeling Effort;79
5.2.1;2.1 Conversion to the EMOD Language;80
5.2.1.1;2.1.1 Unparameterization;81
5.2.1.2;2.1.2 Declaring Implicit and Port Wires;81
5.2.1.3;2.1.3 Standardizing Argument Lists;81
5.2.1.4;2.1.4 Resolving Ranges;81
5.2.1.5;2.1.5 Operator Rewriting;82
5.2.1.6;2.1.6 Sign and Width Computation;82
5.2.1.7;2.1.7 Expression Splitting;82
5.2.1.8;2.1.8 Making Truncation Explicit;82
5.2.1.9;2.1.9 Eliminating Assignments;83
5.2.1.10;2.1.10 Eliminating Instance Arrays;83
5.2.1.11;2.1.11 Eliminating Higher-Arity Gates;83
5.2.2;2.2 Modeling Flow;84
5.3;3 Verification Method;84
5.3.1;3.1 Case-Splitting and Parametrization;86
5.3.2;3.2 Symbolic Simulation of the Hardware Model;86
5.3.3;3.3 Symbolic Simulation of Specification;87
5.3.4;3.4 Comparison of Specification to Hardware Model;88
5.4;4 Mechanisms Used to Achieve the Verification;89
5.4.1;4.1 EMOD Symbolic Simulator;89
5.4.2;4.2 BDDs and AIGs;90
5.4.3;4.3 Parametrization;90
5.4.4;4.4 AIG-to-BDD Translation;91
5.4.5;4.5 GL Symbolic Execution Framework;92
5.5;5 Verification Results and Observations;95
5.6;6 Related Work;96
5.7;7 Conclusion;97
5.8;References;97
6;Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol;99
6.1;1 Introduction;99
6.1.1;1.1 Outline;100
6.2;2 Cryptol Overview;100
6.2.1;2.1 Language Features;100
6.2.1.1;2.1.1 Function Values and Anonymous Functions;100
6.2.1.2;2.1.2 Types and Polymorphism;101
6.2.1.3;2.1.3 Type Aliases and Records;103
6.2.1.4;2.1.4 Enumerations;104
6.2.1.5;2.1.5 Index Operators;104
6.2.1.6;2.1.6 Sequence Operations and Transformations;105
6.2.2;2.2 Cryptol Interpreter;106
6.2.3;2.3 Cryptol Interpreter Modes for Hardware Design;107
6.2.4;2.4 Equivalence Checking;108
6.3;3 Cryptol for Hardware Design;109
6.3.1;3.1 Issues and Limitations;109
6.3.1.1;3.1.1 Supported Subset;109
6.3.1.2;3.1.2 Inefficient Sequence Comprehensions;110
6.3.2;3.2 Combinatorial and Sequential Circuits in Cryptol;111
6.3.3;3.3 Delays and Undelays;113
6.3.4;3.4 Space–Time Tradeoffs via par and seq Pragmas;114
6.3.4.1;3.4.1 Example 1: Parallel Sequence Comprehension;115
6.3.4.2;3.4.2 Example 2: Sequential Sequence Comprehension;117
6.3.5;3.5 Pipelining;118
6.3.5.1;3.5.1 Example 1: Combinatorial Circuit;119
6.3.5.2;3.5.2 Pipelining via the reg Pragma;122
6.4;4 AES Specification;123
6.4.1;4.1 API;123
6.4.2;4.2 Types;124
6.4.3;4.3 Conversions Between Types;126
6.4.4;4.4 Constructors for the Duo Type;126
6.4.5;4.5 Mathematical Preliminaries;126
6.4.5.1;4.5.1 Addition;126
6.4.6;4.6 Multiplication;127
6.4.6.1;4.6.1 Multiplication by x;127
6.4.7;4.7 Polynomials with Coefficients in GF(28);127
6.4.8;4.8 Algorithm Specification;128
6.4.9;4.9 Cipher;128
6.4.9.1;4.9.1 SubBytes() Transformation;129
6.4.9.2;4.9.2 ShiftRows() Transformation;130
6.4.9.3;4.9.3 MixColumns() Transformation;130
6.4.9.4;4.9.4 AddRoundKey() Transformation;131
6.4.10;4.10 Key Expansion;131
6.4.11;4.11 Inverse Cipher;132
6.4.11.1;4.11.1 InvShiftRows() Transformation;132
6.4.11.2;4.11.2 InvSubBytes() Transformation;132
6.4.11.3;4.11.3 InvMixColumns() Transformation;133
6.4.11.4;4.11.4 Equivalent Inverse Cipher;133
6.4.12;4.12 Auxiliary Definitions;134
6.4.13;4.13 Key Expansion Example: 128-bit Cipher Key;136
6.4.14;4.14 Test and Verification;137
6.4.14.1;4.14.1 Example Vectors;137
6.4.14.2;4.14.2 Formal Verification;138
6.5;5 AES Implementations;138
6.5.1;5.1 Implementation #1;139
6.5.2;5.2 Implementation #2;143
6.5.2.1;5.2.1 Implementation #2 Optimized for Area;144
6.5.2.2;5.2.2 Implementation #2 Pipelined Using the reg Pragma;145
6.5.3;5.3 T-Box Implementation;146
6.5.3.1;5.3.1 T-Box Implementation Optimized for Area;147
6.5.3.2;5.3.2 T-Box Implementation Pipelined Using the reg Pragma;148
6.5.4;5.4 Testing and Verification;150
6.5.5;5.5 Performance;151
6.6;6 Conclusion;152
6.7;References;153
7;Verifying Pipelines with BAT;154
7.1;1 Introduction;154
7.2;2 Bit-Level Analysis Tool;155
7.2.1;2.1 BAT Specification Language;156
7.2.1.1;2.1.1 Data Types;156
7.2.1.2;2.1.2 Primitives;157
7.2.1.3;2.1.3 Expressions;157
7.2.1.4;2.1.4 User-Defined Functions;159
7.2.1.5;2.1.5 Specification Formats;159
7.2.1.6;2.1.6 Other Language Features;160
7.2.2;2.2 BAT Decision Procedure;160
7.2.2.1;2.2.1 Memory Abstraction;160
7.2.2.2;2.2.2 Efficient Translation To CNF;161
7.3;3 ISA and Pipelined Machine Models;161
7.3.1;3.1 ISA Definition;163
7.3.2;3.2 MA Definition;166
7.4;4 Refinement;171
7.5;5 Verification;175
7.5.1;5.1 Refinement Map Definitions;176
7.6;6 Scaling to More Complex Designs;179
7.6.1;6.1 Efficient Refinement Maps;180
7.6.2;6.2 Compositional Reasoning;180
7.6.3;6.3 Combining Theorem Proving and Decision Procedures;180
7.6.4;6.4 Parametrization;181
7.7;7 Conclusions;181
7.8;References;182
8;Formal Verification of Partition Management for the AAMP7G Microprocessor;184
8.1;1 Introduction;184
8.2;2 The AAMP7G Microprocessor;185
8.2.1;2.1 AAMP7G Intrinsic Partitioning;185
8.2.1.1;2.1.1 Time Partitioning;186
8.2.1.2;2.1.2 Space Partitioning;186
8.2.2;2.2 Partition Control;187
8.3;3 AAMP7G Formal Processing Model;188
8.4;4 A Formal Security Specification;189
8.4.1;4.1 The Formal Security Specification in ACL2;190
8.4.2;4.2 An AAMP7G Instantiation of GWV;193
8.4.3;4.3 Proof of the AAMP7G Instantiation of GWV;195
8.5;5 Use of Formal Analysis in a Certification;196
8.6;6 Formalization within a Partition: The AAMP7G Instruction Set Model;197
8.6.1;6.1 Instruction Set Model Validation;198
8.6.2;6.2 Abstract Instruction Set Modeling and Symbolic Simulation;198
8.6.3;6.3 Compositional Code Proof;199
8.7;7 Conclusion;199
8.8;References;200
9;Compiling Higher Order Logic by Proof;201
9.1;1 Compilation and Logic;201
9.1.1;1.1 A Gap Between Program Verification and Compiler Verification;202
9.1.2;1.2 Compilation by Proof;203
9.2;2 Higher Order Logic;203
9.2.1;2.1 Deductive System;205
9.2.2;2.2 Definitions;206
9.2.3;2.3 The HOL4 Proof Environment;207
9.2.3.1;2.3.1 Proof Techniques;208
9.2.3.2;2.3.2 Custom Proof Procedures;208
9.2.3.3;2.3.3 Theories and Libraries;209
9.2.3.4;2.3.4 External Interfaces;209
9.2.3.5;2.3.5 Applications;210
9.3;3 Source Language: TFL;211
9.4;4 Compilation by Rewriting;212
9.4.1;4.1 Pattern Matching;213
9.4.2;4.2 Polymorphism;215
9.4.3;4.3 Sequentialization via CPS;218
9.4.4;4.4 Defunctionalization;219
9.4.5;4.5 Register Allocation;221
9.5;5 Engaging with the Machine;224
9.6;6 Related Work;224
9.7;7 Conclusions and Future Work;225
9.8;References;226
10;Specification and Verification of ARM Hardware and Software;229
10.1;1 Introduction and Overview;229
10.2;2 Specification and Verification of ARM Architectures;232
10.2.1;2.1 The Swansea Methodology;232
10.2.2;2.2 Starting at Cambridge;233
10.2.3;2.3 Modelling the ARM Instruction Set Architecture;233
10.2.3.1;2.3.1 The State Space;234
10.2.4;2.4 Modelling the ARM6 Micro-Architecture;235
10.2.4.1;2.4.1 Coverage;236
10.2.4.2;2.4.2 Input and Output;236
10.2.5;2.5 Beyond the ARM6;237
10.2.5.1;2.5.1 Further Refinements;238
10.2.6;2.6 Going Monadic;238
10.2.6.1;2.6.1 Coverage;240
10.2.6.2;2.6.2 Single-Step Theorems;241
10.2.6.3;2.6.3 Active and Future Work;242
10.3;3 High-Assurance Software Engineering;242
10.3.1;3.1 Machine-Code Hoare Logic;243
10.3.1.1;3.1.1 Set-Based Separating Conjunction;244
10.3.1.2;3.1.2 Definition of Hoare Triple;245
10.3.1.3;3.1.3 Proof Rules;246
10.3.2;3.2 Decompilation of ARM Code;247
10.3.2.1;3.2.1 Example;247
10.3.2.2;3.2.2 Implementation;248
10.3.3;3.3 Extensible Proof-Producing Compilation;249
10.3.3.1;3.3.1 Example 1;249
10.3.3.2;3.3.2 Example 2;250
10.3.3.3;3.3.3 Implementation;250
10.3.4;3.4 Case Study: Verified LISP Interpreter;251
10.3.4.1;3.4.1 Example;251
10.3.4.2;3.4.2 LISP Evaluation;252
10.3.4.3;3.4.3 Parsing and Printing;253
10.3.4.4;3.4.4 Final Correctness Theorem;253
10.4;4 Conclusions and Future Research;253
10.5;References;254
11;Information Security Modeling and Analysis;256
11.1;1 Introduction;256
11.1.1;1.1 Formal PVS Specifications;256
11.2;2 A Formal Model of Computing Systems;257
11.2.1;2.1 A Formal Model of Information;257
11.2.1.1;2.1.1 The Calculus of Indices;258
11.2.1.2;2.1.2 Paths;260
11.2.1.3;2.1.3 A Simple Calculus in PVS;260
11.2.1.4;2.1.4 Properties of Basis Sets;261
11.2.2;2.2 A Formal Model of Communication;264
11.2.2.1;2.2.1 Congruences in PVS;265
11.2.2.2;2.2.2 Information Flow as a Graph;266
11.2.2.3;2.2.3 Graphs in PVS;267
11.2.2.4;2.2.4 Graph Functions;268
11.2.2.5;2.2.5 GWVr1 in PVS;269
11.2.3;2.3 Examples of Applying GWVr1;271
11.2.4;2.4 Graph Composition;277
11.2.4.1;2.4.1 Graph Composition in PVS;277
11.2.5;2.5 Graph Abstraction;280
11.2.6;2.6 GWVr1 and Guarded Domains;282
11.3;3 GWVr2;285
11.3.1;3.1 GWVr2 Reduction;288
11.3.2;3.2 Domain Guards and GWVr2;290
11.4;4 Multicycle Information Flow Analysis;292
11.5;5 Classical Noninterference;296
11.5.1;5.1 Domains;297
11.5.2;5.2 Capabilities;297
11.5.3;5.3 Noninterference Example in PVS;297
11.5.4;5.4 Establishing the Noninterference Property;300
11.6;6 Conclusion;304
11.7;References;305
12;Modeling and Security Analysis of a Commercial Real-Time Operating System Kernel;307
12.1;1 Introduction;307
12.2;2 Separation Theorem;309
12.3;3 Modeling System State;311
12.4;4 Modeling Kernel Behavior;313
12.4.1;4.1 Reader Macro;314
12.4.1.1;4.1.1 Global Variable Access;314
12.4.1.2;4.1.2 Assignment;314
12.4.1.3;4.1.3 Functions;315
12.4.1.4;4.1.4 Conditional Early Exit;315
12.4.2;4.2 Model Example;316
12.4.3;4.3 Model Syntax Summary;317
12.4.4;4.4 Kernel Boundaries;320
12.4.4.1;4.4.1 Breaking the Kernel Loop;320
12.4.4.2;4.4.2 Hardware-Dependent Layer;321
12.4.4.3;4.4.3 Interrupt Processing;322
12.4.4.4;4.4.4 Application Software Execution;322
12.5;5 Modeling Information Flow;322
12.5.1;5.1 Crawlers;323
12.5.2;5.2 Graphs;323
12.5.3;5.3 Graph Composition;324
12.6;6 Proof of Separation;325
12.6.1;6.1 Workhorse Lemma;325
12.6.2;6.2 ClearP Lemma;326
12.7;7 Hardware-Dependent Code Analysis;327
12.8;8 Conclusion;327
12.9;References;327
13;Refinement in the Formal Verification of the seL4 Microkernel;329
13.1;1 Introduction;329
13.2;2 Data Refinement;330
13.2.1;2.1 Forward Simulation;331
13.2.2;2.2 Structure;332
13.2.3;2.3 Correspondence;333
13.3;3 Example;334
13.4;4 Monadic Refinement;335
13.4.1;4.1 Non-deterministic State Monads;335
13.4.2;4.2 Correspondence;335
13.4.3;4.3 Mapping to Processes;337
13.5;5 C Refinement;337
13.5.1;5.1 Refinement Calculus for C;339
13.5.2;5.2 The Correspondence Statement;339
13.5.3;5.3 Proving Correspondence via the VCG;341
13.5.4;5.4 Splitting;341
13.5.5;5.5 Mapping to Processes;342
13.6;6 Main Theorem;342
13.7;7 Related Work;343
13.8;8 Conclusion;343
13.9;References;344
14;Specification and Checking of Software Contracts for Conditional Information Flow;346
14.1;1 Introduction;346
14.2;2 Example ;348
14.3;3 Foundations of SPARK Conditional Information Flow;350
14.3.1;3.1 Semantics;351
14.3.2;3.2 Reasoning About Information Flow in Terms of Noninterference;352
14.3.3;3.3 Capturing Noninterference and Secure Information Flow in a Compositional Logic;352
14.3.4;3.4 Relations Between Agreement Assertions;354
14.4;4 Conditional Information Flow Contracts;354
14.4.1;4.1 Foundations of Flow Contracts;354
14.4.2;4.2 Language Design for Conditional SPARK Contracts;355
14.4.2.1;4.2.1 Simplifying Assertions;355
14.4.2.2;4.2.2 Design Methodology Separating Guard Logic from Flow Logic;356
14.4.2.3;4.2.3 Contract Abstraction and Refinement;357
14.5;5 A Precondition Generation Algorithm;357
14.5.1;5.1 Correctness Results;358
14.5.2;5.2 Intraprocedural Analysis;359
14.5.3;5.3 Interprocedural Analysis;360
14.5.4;5.4 Synthesizing Loop Invariants;361
14.6;6 Evaluation;363
14.6.1;6.1 Summary of Performance;363
14.6.1.1;6.1.1 Code Bases;364
14.6.1.2;6.1.2 Typical Refinement Power of the Algorithm;364
14.6.1.3;6.1.3 Efficiency of Inference Algorithm;366
14.6.1.4;6.1.4 Sources of Loss of Precision;366
14.6.1.5;6.1.5 Threats to Validity of Experiments;366
14.6.2;6.2 Detailed Discussion of Selected Examples;367
14.6.2.1;6.2.1 Mailbox Example;367
14.6.2.2;6.2.2 Autopilot Example;370
14.7;7 Related Work;381
14.8;8 Conclusion;382
14.9;References;383
15;Model Checking Information Flow;385
15.1;1 Introduction;385
15.2;2 A Motivating Example;386
15.2.1;2.1 Shared Buffer Simulink Model;388
15.3;3 Information Flow Modeling for Synchronous Dataflow Languages;390
15.3.1;3.1 Modeling Information Flow;392
15.3.2;3.2 Using PVS;393
15.3.3;3.3 Traces and Processes;393
15.3.4;3.4 Semantic Rule Conventions;396
15.3.5;3.5 Value Trace Semantics;397
15.3.6;3.6 Creating an Accurate Model of Information Flow;397
15.3.7;3.7 PVS Proof of Trace Equivalence (InterferenceTheorem);401
15.3.7.1;3.7.1 Expression Equivalence Theorems;403
15.3.7.2;3.7.2 Program Well-Formedness Theorems;403
15.3.7.3;3.7.3 GWV Equivalence Theorems;403
15.3.7.4;3.7.4 Proof of InterferenceTheorem;406
15.4;4 Interference to Noninterference;407
15.5;5 Model Checking Information Flow;408
15.5.1;5.1 Formalizing Noninterference in LTL;410
15.5.2;5.2 Creating the Information Flow Model;410
15.5.3;5.3 From Principals to Domains;414
15.5.4;5.4 Adding Control Variables;416
15.6;6 Intransitive Interference and Noninterference;416
15.6.1;6.1 Formulating Intransitive Interference;417
15.6.1.1;6.1.1 The Problem of Implicit Functional Dependencies;417
15.6.1.2;6.1.2 An Overly Conservative Formulation;418
15.6.2;6.2 Modeling Intransitive Interference Using Graph Cuts;418
15.7;7 Connections to GWV;420
15.7.1;7.1 From InterferenceTheorem to GWVr1;421
15.8;8 Using Gryphon for Information Flow Analysis;423
15.8.1;8.1 Model-Based Development ToolChain;423
15.8.1.1;8.1.1 Simulink, Stateflow, MATLAB;423
15.8.1.2;8.1.2 Reactis;423
15.8.1.3;8.1.3 Gryphon;424
15.8.1.4;8.1.4 Prover;425
15.8.1.5;8.1.5 Custom Code Generation;425
15.8.2;8.2 Modeling and Analyzing the Turnstile High-Assurance Guard Architecture;425
15.8.2.1;8.2.1 Representing the Turnstile Architecture in Simulink;427
15.9;9 Conclusion and Future Work;429
15.9.1;9.1 Future Work;430
15.10;References;431
16;Index;433