[SystemSafety] Machine models under formal methods

David MENTRÉ David.MENTRE at bentobako.org
Sat Nov 11 21:41:38 CET 2017


Dear Mr Carpenter,

Preamble: in this discussion on formal methods, formal methods
proponents have never said this is THE answer to all safety issues. It
is just a tool as part of the safety toolbox, sometimes a better tool
than others. This tool should be at least *considered*.

Le 2017-11-10 à 15:39, Todd Carpenter a écrit :
> But those instruction sets are often backed by microcode, which was not
> developed under formal methods.

Probably true for most of processors, but there are some recent and
pretty interesting efforts like formal specification of ARM-v8
architecture by ARM:
  https://alastairreid.github.io/alastairreid.github.io/ARM-v8a-xml-release/

Some excerpts of paper abstracts:
  https://alastairreid.github.io/papers/CAV_16/
"""
This is an end-to-end framework to detect bugs in the datapath, pipeline
control and forwarding/stall logic of processors.
[...]
We have applied this method to 8 different ARM processors spanning all
stages of development up to release. In all processors, this has found
bugs that would have been hard for conventional simulation-based
verification to find and ISA-Formal is now a key part of ARM's formal
verification strategy.
"""

And for those wondering how a formal specification can match the real world:
  https://alastairreid.github.io/papers/OOPSLA_17/
"""
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.
[...]
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.
"""

This work is not a *complete* specification of ARM architecture, but a
focused effort on a significant subset of that architecture.


It is also known for a long time that Intel and AMD formally verify part
of their processors, like their Floating-Point Units. It appears that
Intel is now having much more ambitious goals (disclaimer: I just
discovered this paper, I don't know much about this work):
  https://is.muni.cz/el/1433/jaro2010/IA159/um/intel.pdf
  Replacing Testing with Formal Verification in Intel Core TM i7
Processor Execution Engine Validation
"""
Formal verification of arithmetic data-paths has been part of the
established methodology for most Intel processor designs over the last
years, usually in the role of supplementing more traditional coverage
oriented testing activities. For the recent Intel  Core TM i7 design we
took a step further and used formal verification as the primary
validation vehicle for the core execution cluster, the component
responsible for the functional behaviour of all microinstructions. We
applied symbolic simulation based formal verification techniques for
full data-path, control and state validation for the cluster, and
dropped coverage driven testing entirely. The project, involving some
twenty person years of verification work, is one of the most ambitious
formal verification efforts in the hardware industry to date. Our
experiences show that under the right circumstances, full formal
verification of a design component is a feasible, industrially viable
and competitive validation approach.
"""

> So now lets assume that we develop processors, MMUs, caches, and
> inter-core networks that are well behaved. It's possible. What happens
> when that machine suffers Single Event Errors?

Some people have developed in the past architectures dedicated to safety
applications, like the Vital Coded Processor that catch such event:
  http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.525.1766&rank=5
"""
With the Vital Coded Processor, any run time error caused either by a
compiler error or a hardware failure is detected and the unit is set in
a safe state.
"""

Nowadays people are developing low cost high-integrity platform for
safety critical application (typically SIL4 of EN50128), like the LCHIP
project:
  http://www.clearsy.com/en/2016/10/4260/

Above effort are for rather simple processors. I don't know any other
effort to offer similar guarantees for more complex architectures with
MMU, DMA, caches, etc. I would be interested to know if they exist.

Sincerely yours,
D. Mentré


More information about the systemsafety mailing list