Software and hardware are increasingly being formally verified against
specifications, but how can we verify the specifications themselves? This paper
explores what it means to formally verify a specification. We solve three
challenges: (1) How to create a secondary, higher-level specification that can
be effectively reviewed by processor designers who are not experts in formal
verification; (2) How to avoid common-mode failures between the specifications;
and (3) How to automatically verify the two specifications against each other.

One of the most important specifications for software verification is the
processor specification since it defines the behaviour of machine code and of
hardware protection features used by operating systems. We demonstrate our
approach on ARM's v8-M Processor Specification, which is intended to improve
the security of Internet of Things devices. Thus, we focus on establishing the
security guarantees the architecture is intended to provide. Despite the fact
that the ARM v8-M specification had previously been extensively tested, we
found twelve bugs (including two security bugs) that have all been fixed by
ARM.

Researcher at Arm Ltd (UK) since 2004

• model checking processor pipelines (newest)
• formal architecture specifications
• wide SIMD instruction set
• pipeline parallelism
• software defined radio
• vectorising compilers (oldest)

Researcher at University of Utah (USA), 1998-2004

• component based operating system kernels

Researcher at Yale University (USA), 1994-1998

• Haskell foreign function interface
• Functional Reactive Programming
• Visual Tracking in Haskell
• Haskell library/compiler development

Researcher at University of Glasgow (UK), 1988-1994

• Formal Specification and Verification
• GHC foreign function interface