Title page
Contents
Executive Summary 6
1. Summary 7
1.1. Purpose 7
1.2. Approach 7
1.3. Overview of This Report 7
2. Background and Problem Statement 8
2.1. Introduction 8
2.2. Problem Statement 8
2.3. Vulnerabilities at the Interfaces 8
3. Technical Approach: Provably Secure Parsers 10
3.1. Verification Properties 10
3.2. Verification Approaches: Overview 11
3.3. Verification Approach 12
3.4. The High-Assurance ASN.1 Workbench 12
3.5. The Software Analysis Workbench 14
3.6. Summary of Approach 15
4. Project Execution 16
4.1. Summary 16
4.2. Tasks 16
4.2.1. Task 1. Analyze SAE J2735 specification in HAAW 16
4.2.1.1. Original Task Description 16
4.2.1.2. Commentary 16
4.2.2. Task 2. Generate C Encoder/Decoder Routines for SAE J2735 17
4.2.2.1. Original Task Description 17
4.2.2.2. Commentary 17
4.2.3. Task 3. Verify Execution Safety of Generated C Code 17
4.2.3.1. Original Task Description 17
4.2.3.2. Commentary 18
4.2.4. Task 4. Verify Functional Correctness of Generated C Code 19
4.2.4.1. Original Task Description 19
4.2.4.2. Commentary 20
5. Conclusions 24
5.1. Assessments 24
5.2. Deliverables 24
Figure 1. HAAW Workflow 13
Figure 2. SAW Workflow 14