# Presentation: 434796

## On the Scalability of Proof Carrying Code for Software Certification

- Andrew Ireland
- School of Mathematical & Computer Sciences
- Heriot-Watt University
- Edinburgh

## Outline

- High integrity software development
- Evidence based software certificates
- Scalability problems
- A planning approach
- Issues for discussion

## The SPARK Approach

- SPARK
- Examiner

- SPADE
- Simplifier

- SPADE
- Proof Checker

-  SPARK is a subset of Ada with annotations
-   (Praxis High Integrity Systems Ltd)
-  Supports data & information flow analysis and
-   formal verification *- *in particular, exception freedom proofs
-  EuroFighter and Hawk projects, advocated by NSA, ...

- VCs

- UnprovenVCs

****

- SPARK
- code

- Proofs

**X**

*Revisions*

- Tactics

## SPARK and Certification

- Z specifications + rigorous proofs
- Data & information flow analysis
- Code level proofs:
- Exception freedom proofs:* automatic + interactive proofs*
- Functional proofs: *significant level of interactive proofs*
- Proof review files
- Resource analysis
- Note: explicit evidence via proof either fragile or absent

## NuSPADE

- SPARK
- Examiner

- SPADE
- Simplifier

- SPADE
- Proof Checker

-  NuSPADE = proof planning + program analysis
-  Annotation generation motivated by proof-failure analysis
-  Proof planning supports a robust style of reasoning, *i.e.*
-   addresses the fragility of interactive proof

- VCs

- UnprovenVCs

****

- SPARK
- code

- Proofs

*Annotations*

**X**

- Tactics

## NuSPADE

- Unproven
- VCs

- Abstract
- Predicates

- Annotations

- Co-operative style of integration,* i.e. “productive use of failure” *

- Proof
- Planner

- Program
- Analyzer

- Tactics

- Evidence Based Certification

- Proof-Carrying Code (PCC) *– a example of an evidence based approach to certification*
- Code is delivered with a certificate containing a condensed mathematical proof, *i.e.* a proof that the code satisfies desired safety properties
- Responsibility for proof construction lies with the code producer, consumer performs proof checking
- Trusted Computing Base (TCB) for PCC is small, *i.e. *safety properties, verification condition generator and proof checker

- Properties, Proofs & Certificates

- Properties typically simple, *e.g.* memory safety
- Proof construction involves advanced type checking, *i.e.* no theorem proving
- Certificates:
- LF proofs quadratic with respect to program size
- LFi proofs 2.5 to 5 times program size
- Oracles strings on average 12% program size
- Proof tactics have also been used

- Scalability Problems

- Need for comprehensive properties, *e.g. *functional properties
- MOBIUS: combining type-based and logic-based approaches
- Need to exploit automated theorem proving techniques
- Will current PCC architecture scale-up, *e.g. oracles strings?*

## Proof Plans

- Conjecture

- Plan

- Theory

- Proof
- Planner

- Proof
- Checker

- Tactic

- Proof

## Proof Plans

- Conjecture

- Plan

- Theory

- Proof
- Planner

- Proof
- Checker

- Tactic

- Proof

## Proof Plans

- Conjecture

- Plan

- Theory

- Proof
- Planner

- Proof
- Checker

- Tactic

- Proof

- Oracle

## Planning Oracles as Certificates

- Conjecture

- Plan

- Theory

- Proof
- Planner

- Proof
- Checker

- Tactic

- Proof

- Oracle

## Planning Oracles as Certificates

- Conjecture

- Plan

- Theory

- Proof
- Planner

- Proof
- Checker

- Tactic

- Proof

- Oracle

**Oracle identifies:**
** ****Proof plans and where they should be used**
** ****Relevant theories**
** ****Search control hints, ***e.g.*** auxiliary lemmas **
**  ****and generalization steps**

## Certificate Generation

- Code +
- Spec

*(VCGen + Planner +Checker)*

- Certificate
*(Oracle)*

**?**

- Proof

- Failure

- Repositories
*(plans + theories)*

## Certificate Validation

- Code +
- Spec

*(VCGen + Planner +Checker)*

- Certificate
*(Oracle)*

- Repositories
*(plans + theories)*

**?**

- Proof

- Failure

- CPU

- Discussion Issues

- The proposed proof planning approach will add theory repositories (and specifications) to the TCB *– **is this acceptable?*
- For memory limited devices, proof planning oracles are not an option for on-device certificate validation *– **how important is on-device validation to certification management in general? *
- More comprehensive properties will require off-device validation – *could a dedicated certificate validation device have a role to play?*
*Certificate transforming compiler or trusted compiler?*

- Conclusion

- The SPARK Approach
- SPARK proofs lack explicit evidence or are fragile
- Proof planning gives rise to fully expansive proofs and increases automation, *i.e.* proofs are explicit and robust
- Building upon the idea of *oracle strings,* we propose the use of *proof planning oracles* as a technique for scaling PCC for general purpose software certification

## Slide 19