Trusting Large Specifications:
The Virtuous Cycle
Alastair Reid
alastair.reid@arm.com@alastair_d_reid

ARMResearchApplica'on
LibraryOS
Compiler
Processor

ARMResearch2

Qualities of a Specification
Applicability
Scope
Trustworthiness

ARMResearch3Applicability
v6 (1997)
A-class (phones/tablets/servers)

v7 (2005)

R-class (real-time, lock-step support)

v8.0 (2013)

M-class (microcontroller)

v8.1 (2015)v8.2 (2016)

ARMResearch4ScopeCompiler targeted instructions?
User-level instructions?
User+Supervisor?
User+Supervisor+Hypervisor+Secure Monitor?

ARMResearch

5

ISA Specification - ASL
OpcodeCheck Validity
Get Operands
Set Result Register
Set Flags
ARMResearch

6System Architecture Specification

ARMResearch

7

ARM Spec (lines of code)
v8-A

v8-M

26,0006,000

Exceptions
Memory

4,000
3,000

3,000
1,000

Debug

3,000

1,000

Misc

5,500

2,000

(Test support)

1,500

2,000

Total

43,00015,000Instructions
Int/FP/SIMD

ARMResearch8System Register Spec

ARMResearch

v8-A

v8-M

Registers

586

186

FieldsConstantaoe
Reserved
Impl. Defined
Passive
ActiveOperations

3951
985
940
70
1888
68112

622
177
208
10165
62109Trustworthiness

ARMResearch10Trustworthiness
ARM’s specification is correct by definition

ARMResearch

10Trustworthiness
ARM’s specification is correct by definition

ARMResearch

10Trustworthiness
Does the specification match the behaviourof all ARM processors?

ARMResearch

11

ARM Spec
Test S'mulus=?=Oracle

ARMResearch

12

ARM Spec

Directed Tests
Random Tests…
Memory Tests
IRQ Generators

ARMResearch=?=Oracle

13

ARM Spec

Directed Tests
Random Tests…
Memory Tests
IRQ Generators

ARMResearchSelf-checking
Bus monitors
Trace compare

Oracle14

Architecture Conformance Suite
Processor architectural compliance sign-off
Large
v8-A 11,000 test programs, > 2 billion instructions
v8-M 3,500 test programs, > 250 million instructions

Thorough
Tests dark corners of specification

ARMResearch

15

v8-A

v8-M

100%

100%

75%

75%

50%

50%

25%

25%

0%

0%

ARMResearch16Trustworthy Speciﬁca'ons of ARM v8-A and v8-M System Level Architecture, FMCAD 2016

Pass / FailARM Spec
ELF Test

ASL Interpreter

Implementa'on
DeﬁnedARMResearch

17End to End Veriﬁca'on of ARM Processors with ISA-Formal, CAV 2016

Counterexample

ARM SpecModelChecker

ARM CPUCounterexample
ARMResearch18

(Work by Jon French and Nathan Chong)

ARM Spec
mbedOSASL Interpreter

Implementa'on
DeﬁnedARMResearch19

(Work by Jon French and Nathan Chong)

ARM Spec

AFL
FuzzermbedOS

Bugs
ARMResearch

20Creating a Virtuous Cycle
Testcase
Genera'on

So_wareVeriﬁca'on

Boot
OS
ARMResearch

21

ARM
Conformance
TestSuite

Informa'on
Flow
Analysis

ARM Spec

Processor
Veriﬁca'on

AFL
FuzzerRandomInstruc'on
SequencesPreparing public release of ARM v8-A specification• Enable formal verification of software and tools• Public release planned for 2016 Q4• Liberal license• REMS group currently translating to SAIL

Talk to me about how I can help you use it
ARMResearch

22CPU Specifications
Basis of a lot of formal verification
Too large to be “obviously correct”
Reusable specs enable “virtuous cycle”
Greater effort to produce
Share testing / maintenance effort
More likely to be correct
Preparing public release of machine readable ARM Specification
ARMResearch

23

EndAlastair Reid
ARMResearch
alastair.reid@arm.com@alastair_d_reid