Design and Verification of Microprocessor Systems for High-Assurance Applications (eBook)

Preface 6
Contents 9
ACL2 and Its Applications to Digital System Verification 13
1 Introduction 13
2 Some Basic Decisions 13
3 ACL2 15
3.1 A Programming Language 16
3.2 A Logical Theory 18
3.3 A Mechanical Theorem Prover and Proof Environment 20
3.4 Efficiency 22
4 A Simple Microprocessor Model 23
5 Variations on the Theme 29
6 Summary 30
References 31
A Mechanically Verified Commercial SRT Divider 34
1 Introduction 34
2 SRT Division 37
3 Quotient Digit Selection 42
4 Implementation 47
4.1 Analysis of Operands 48
4.2 Iteration 52
4.3 Final Computation 58
References 64
Use of Formal Verification at Centaur Technology 75
1 Introduction 75
1.1 Overview of Verification Methodology 75
1.2 Timeline 76
1.3 Centaur Media Unit 78
2 Modeling Effort 79
2.1 Conversion to the EMOD Language 80
2.1.1 Unparameterization 81
2.1.2 Declaring Implicit and Port Wires 81
2.1.3 Standardizing Argument Lists 81
2.1.4 Resolving Ranges 81
2.1.5 Operator Rewriting 82
2.1.6 Sign and Width Computation 82
2.1.7 Expression Splitting 82
2.1.8 Making Truncation Explicit 82
2.1.9 Eliminating Assignments 83
2.1.10 Eliminating Instance Arrays 83
2.1.11 Eliminating Higher-Arity Gates 83
2.2 Modeling Flow 84
3 Verification Method 84
3.1 Case-Splitting and Parametrization 86
3.2 Symbolic Simulation of the Hardware Model 86
3.3 Symbolic Simulation of Specification 87
3.4 Comparison of Specification to Hardware Model 88
4 Mechanisms Used to Achieve the Verification 89
4.1 EMOD Symbolic Simulator 89
4.2 BDDs and AIGs 90
4.3 Parametrization 90
4.4 AIG-to-BDD Translation 91
4.5 GL Symbolic Execution Framework 92
5 Verification Results and Observations 95
6 Related Work 96
7 Conclusion 97
References 97
Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol 99
1 Introduction 99
1.1 Outline 100
2 Cryptol Overview 100
2.1 Language Features 100
2.1.1 Function Values and Anonymous Functions 100
2.1.2 Types and Polymorphism 101
2.1.3 Type Aliases and Records 103
2.1.4 Enumerations 104
2.1.5 Index Operators 104
2.1.6 Sequence Operations and Transformations 105
2.2 Cryptol Interpreter 106
2.3 Cryptol Interpreter Modes for Hardware Design 107
2.4 Equivalence Checking 108
3 Cryptol for Hardware Design 109
3.1 Issues and Limitations 109
3.1.1 Supported Subset 109
3.1.2 Inefficient Sequence Comprehensions 110
3.2 Combinatorial and Sequential Circuits in Cryptol 111
3.3 Delays and Undelays 113
3.4 Space–Time Tradeoffs via par and seq Pragmas 114
3.4.1 Example 1: Parallel Sequence Comprehension 115
3.4.2 Example 2: Sequential Sequence Comprehension 117
3.5 Pipelining 118
3.5.1 Example 1: Combinatorial Circuit 119
3.5.2 Pipelining via the reg Pragma 122
4 AES Specification 123
4.1 API 123
4.2 Types 124
4.3 Conversions Between Types 126
4.4 Constructors for the Duo Type 126
4.5 Mathematical Preliminaries 126
4.5.1 Addition 126
4.6 Multiplication 127
4.6.1 Multiplication by x 127
4.7 Polynomials with Coefficients in GF(28) 127
4.8 Algorithm Specification 128
4.9 Cipher 128
4.9.1 SubBytes() Transformation 129
4.9.2 ShiftRows() Transformation 130
4.9.3 MixColumns() Transformation 130
4.9.4 AddRoundKey() Transformation 131
4.10 Key Expansion 131
4.11 Inverse Cipher 132
4.11.1 InvShiftRows() Transformation 132
4.11.2 InvSubBytes() Transformation 132
4.11.3 InvMixColumns() Transformation 133
4.11.4 Equivalent Inverse Cipher 133
4.12 Auxiliary Definitions 134
4.13 Key Expansion Example: 128-bit Cipher Key 136
4.14 Test and Verification 137
4.14.1 Example Vectors 137
4.14.2 Formal Verification 138
5 AES Implementations 138
5.1 Implementation #1 139
5.2 Implementation #2 143
5.2.1 Implementation #2 Optimized for Area 144
5.2.2 Implementation #2 Pipelined Using the reg Pragma 145
5.3 T-Box Implementation 146
5.3.1 T-Box Implementation Optimized for Area 147
5.3.2 T-Box Implementation Pipelined Using the reg Pragma 148
5.4 Testing and Verification 150
5.5 Performance 151
6 Conclusion 152
References 153
Verifying Pipelines with BAT 154
1 Introduction 154
2 Bit-Level Analysis Tool 155
2.1 BAT Specification Language 156
2.1.1 Data Types 156
2.1.2 Primitives 157
2.1.3 Expressions 157
2.1.4 User-Defined Functions 159
2.1.5 Specification Formats 159
2.1.6 Other Language Features 160
2.2 BAT Decision Procedure 160
2.2.1 Memory Abstraction 160
2.2.2 Efficient Translation To CNF 161
3 ISA and Pipelined Machine Models 161
3.1 ISA Definition 163
3.2 MA Definition 166
4 Refinement 171
5 Verification 175
5.1 Refinement Map Definitions 176
6 Scaling to More Complex Designs 179
6.1 Efficient Refinement Maps 180
6.2 Compositional Reasoning 180
6.3 Combining Theorem Proving and Decision Procedures 180
6.4 Parametrization 181
7 Conclusions 181
References 182
Formal Verification of Partition Management for the AAMP7G Microprocessor 184
1 Introduction 184
2 The AAMP7G Microprocessor 185
2.1 AAMP7G Intrinsic Partitioning 185
2.1.1 Time Partitioning 186
2.1.2 Space Partitioning 186
2.2 Partition Control 187
3 AAMP7G Formal Processing Model 188
4 A Formal Security Specification 189
4.1 The Formal Security Specification in ACL2 190
4.2 An AAMP7G Instantiation of GWV 193
4.3 Proof of the AAMP7G Instantiation of GWV 195
5 Use of Formal Analysis in a Certification 196
6 Formalization within a Partition: The AAMP7G Instruction Set Model 197
6.1 Instruction Set Model Validation 198
6.2 Abstract Instruction Set Modeling and Symbolic Simulation 198
6.3 Compositional Code Proof 199
7 Conclusion 199
References 200
Compiling Higher Order Logic by Proof 201
1 Compilation and Logic 201
1.1 A Gap Between Program Verification and Compiler Verification 202
1.2 Compilation by Proof 203
2 Higher Order Logic 203
2.1 Deductive System 205
2.2 Definitions 206
2.3 The HOL4 Proof Environment 207
2.3.1 Proof Techniques 208
2.3.2 Custom Proof Procedures 208
2.3.3 Theories and Libraries 209
2.3.4 External Interfaces 209
2.3.5 Applications 210
3 Source Language: TFL 211
4 Compilation by Rewriting 212
4.1 Pattern Matching 213
4.2 Polymorphism 215
4.3 Sequentialization via CPS 218
4.4 Defunctionalization 219
4.5 Register Allocation 221
5 Engaging with the Machine 224
6 Related Work 224
7 Conclusions and Future Work 225
References 226
Specification and Verification of ARM Hardware and Software 229
1 Introduction and Overview 229
2 Specification and Verification of ARM Architectures 232
2.1 The Swansea Methodology 232
2.2 Starting at Cambridge 233
2.3 Modelling the ARM Instruction Set Architecture 233
2.3.1 The State Space 234
2.4 Modelling the ARM6 Micro-Architecture 235
2.4.1 Coverage 236
2.4.2 Input and Output 236
2.5 Beyond the ARM6 237
2.5.1 Further Refinements 238
2.6 Going Monadic 238
2.6.1 Coverage 240
2.6.2 Single-Step Theorems 241
2.6.3 Active and Future Work 242
3 High-Assurance Software Engineering 242
3.1 Machine-Code Hoare Logic 243
3.1.1 Set-Based Separating Conjunction 244
3.1.2 Definition of Hoare Triple 245
3.1.3 Proof Rules 246
3.2 Decompilation of ARM Code 247
3.2.1 Example 247
3.2.2 Implementation 248
3.3 Extensible Proof-Producing Compilation 249
3.3.1 Example 1 249
3.3.2 Example 2 250
3.3.3 Implementation 250
3.4 Case Study: Verified LISP Interpreter 251
3.4.1 Example 251
3.4.2 LISP Evaluation 252
3.4.3 Parsing and Printing 253
3.4.4 Final Correctness Theorem 253
4 Conclusions and Future Research 253
References 254
Information Security Modeling and Analysis 256
1 Introduction 256
1.1 Formal PVS Specifications 256
2 A Formal Model of Computing Systems 257
2.1 A Formal Model of Information 257
2.1.1 The Calculus of Indices 258
2.1.2 Paths 260
2.1.3 A Simple Calculus in PVS 260
2.1.4 Properties of Basis Sets 261
2.2 A Formal Model of Communication 264
2.2.1 Congruences in PVS 265
2.2.2 Information Flow as a Graph 266
2.2.3 Graphs in PVS 267
2.2.4 Graph Functions 268
2.2.5 GWVr1 in PVS 269
2.3 Examples of Applying GWVr1 271
2.4 Graph Composition 277
2.4.1 Graph Composition in PVS 277
2.5 Graph Abstraction 280
2.6 GWVr1 and Guarded Domains 282
3 GWVr2 285
3.1 GWVr2 Reduction 288
3.2 Domain Guards and GWVr2 290
4 Multicycle Information Flow Analysis 292
5 Classical Noninterference 296
5.1 Domains 297
5.2 Capabilities 297
5.3 Noninterference Example in PVS 297
5.4 Establishing the Noninterference Property 300
6 Conclusion 304
References 305
Modeling and Security Analysis of a Commercial Real-Time Operating System Kernel 307
1 Introduction 307
2 Separation Theorem 309
3 Modeling System State 311
4 Modeling Kernel Behavior 313
4.1 Reader Macro 314
4.1.1 Global Variable Access 314
4.1.2 Assignment 314
4.1.3 Functions 315
4.1.4 Conditional Early Exit 315
4.2 Model Example 316
4.3 Model Syntax Summary 317
4.4 Kernel Boundaries 320
4.4.1 Breaking the Kernel Loop 320
4.4.2 Hardware-Dependent Layer 321
4.4.3 Interrupt Processing 322
4.4.4 Application Software Execution 322
5 Modeling Information Flow 322
5.1 Crawlers 323
5.2 Graphs 323
5.3 Graph Composition 324
6 Proof of Separation 325
6.1 Workhorse Lemma 325
6.2 ClearP Lemma 326
7 Hardware-Dependent Code Analysis 327
8 Conclusion 327
References 327
Refinement in the Formal Verification of the seL4 Microkernel 329
1 Introduction 329
2 Data Refinement 330
2.1 Forward Simulation 331
2.2 Structure 332
2.3 Correspondence 333
3 Example 334
4 Monadic Refinement 335
4.1 Non-deterministic State Monads 335
4.2 Correspondence 335
4.3 Mapping to Processes 337
5 C Refinement 337
5.1 Refinement Calculus for C 339
5.2 The Correspondence Statement 339
5.3 Proving Correspondence via the VCG 341
5.4 Splitting 341
5.5 Mapping to Processes 342
6 Main Theorem 342
7 Related Work 343
8 Conclusion 343
References 344
Specification and Checking of Software Contracts for Conditional Information Flow 346
1 Introduction 346
2 Example 348
3 Foundations of SPARK Conditional Information Flow 350
3.1 Semantics 351
3.2 Reasoning About Information Flow in Terms of Noninterference 352
3.3 Capturing Noninterference and Secure Information Flow in a Compositional Logic 352
3.4 Relations Between Agreement Assertions 354
4 Conditional Information Flow Contracts 354
4.1 Foundations of Flow Contracts 354
4.2 Language Design for Conditional SPARK Contracts 355
4.2.1 Simplifying Assertions 355
4.2.2 Design Methodology Separating Guard Logic from Flow Logic 356
4.2.3 Contract Abstraction and Refinement 357
5 A Precondition Generation Algorithm 357
5.1 Correctness Results 358
5.2 Intraprocedural Analysis 359
5.3 Interprocedural Analysis 360
5.4 Synthesizing Loop Invariants 361
6 Evaluation 363
6.1 Summary of Performance 363
6.1.1 Code Bases 364
6.1.2 Typical Refinement Power of the Algorithm 364
6.1.3 Efficiency of Inference Algorithm 366
6.1.4 Sources of Loss of Precision 366
6.1.5 Threats to Validity of Experiments 366
6.2 Detailed Discussion of Selected Examples 367
6.2.1 Mailbox Example 367
6.2.2 Autopilot Example 370
7 Related Work 381
8 Conclusion 382
References 383
Model Checking Information Flow 385
1 Introduction 385
2 A Motivating Example 386
2.1 Shared Buffer Simulink Model 388
3 Information Flow Modeling for Synchronous Dataflow Languages 390
3.1 Modeling Information Flow 392
3.2 Using PVS 393
3.3 Traces and Processes 393
3.4 Semantic Rule Conventions 396
3.5 Value Trace Semantics 397
3.6 Creating an Accurate Model of Information Flow 397
3.7 PVS Proof of Trace Equivalence (InterferenceTheorem) 401
3.7.1 Expression Equivalence Theorems 403
3.7.2 Program Well-Formedness Theorems 403
3.7.3 GWV Equivalence Theorems 403
3.7.4 Proof of InterferenceTheorem 406
4 Interference to Noninterference 407
5 Model Checking Information Flow 408
5.1 Formalizing Noninterference in LTL 410
5.2 Creating the Information Flow Model 410
5.3 From Principals to Domains 414
5.4 Adding Control Variables 416
6 Intransitive Interference and Noninterference 416
6.1 Formulating Intransitive Interference 417
6.1.1 The Problem of Implicit Functional Dependencies 417
6.1.2 An Overly Conservative Formulation 418
6.2 Modeling Intransitive Interference Using Graph Cuts 418
7 Connections to GWV 420
7.1 From InterferenceTheorem to GWVr1 421
8 Using Gryphon for Information Flow Analysis 423
8.1 Model-Based Development ToolChain 423
8.1.1 Simulink, Stateflow, MATLAB 423
8.1.2 Reactis 423
8.1.3 Gryphon 424
8.1.4 Prover 425
8.1.5 Custom Code Generation 425
8.2 Modeling and Analyzing the Turnstile High-Assurance Guard Architecture 425
8.2.1 Representing the Turnstile Architecture in Simulink 427
9 Conclusion and Future Work 429
9.1 Future Work 430
References 431
Index 433