[sw-dev] ISO26262/Safety Consideration for RISC-V Tool Chain?
324 views
Skip to first unread message
Chuang Feng
May 29, 2016, 11:22:06 PM5/29/16
to sw-...@groups.riscv.org
Dear all,
Is anyone already looking at it? This would be useful for automotive market.
Thanks!
Chuang Feng
This email message is for the sole use of the intended recipient(s) and may
contain confidential information. Any unauthorized review, use, disclosure
or distribution is prohibited. If you are not the intended recipient,
please contact the sender by reply email and destroy all copies of the original
message.
Jeremy
May 30, 2016, 5:00:22 AM5/30/16
to RISC-V SW Dev
On Monday, 30 May 2016 04:22:06 UTC+1, chuangf wrote:
Dear all,
Is anyone already looking at it? This would be useful for automotive market.
Hi Chuang,
We started some initial investigation of general safety-integrity levels (SIL) for compilers earlier this year. To get the highest SIL ratings (SIL-3, equivalent to ISO 26262 ASIL-D) you need to have complete control over the construction and history of the software. Realistically this is not possible for an open source tool chain, which would be based on GCC or LLVM.
For tool chains the analysis is also more complex, because in general we are not looking at the safety of the tool chain, but the safety of the code it generates.
However...
For systems which have not been designed from scratch according to ISO 26262 (or more generically IEC 61508) It is possible to get to SIL-2 (ASIL-B/C) through what is described as Proven in Use. This is intended precisely to support functional safety analysis and certification of pre-existing systems. Proven in Use analysis requires sufficient operational hours, revision history, fault reporting systems etc to determine if there is evidence of systematic design faults in the software. This might be achievable for an open source compiler, although it would almost certainly require a fixed release for a particular target architecture and host system. The need for sufficient operating hours means that it is quite likely that by the time any particular compiler release is certified, it is quite old.
Integrity analysis also includes the concept of composition, where you have two independently designed components for the same functionality, each switching to the other in the event of compiler. Thus two SIL-2 systems when suitably composed, can become a SIL-3 system. This raises the intriguing possibility of achieving a SIL-3 open source tool chain by composition of SIL-2 LLVM and GCC tool chains, or a SIL-2 open source tool chain by componsition of two SIL-1 tool chains. At this stage we have done no more work on investigating this (the commercial driver for this investigation did not progress further). It is far from clear how composition would work for tool chains, or even if it can apply to a tool chain.
HTH,
Jeremy
--
Tel: +44 (1590) 610184
Cell: +44 (7970) 676050
SkypeID: jeremybennett
Twitter: @jeremypbennett
Email: jeremy....@embecosm.com
Web: www.embecosm.com
PGP key: 1024D/BEF58172FB4754E1 2009-03-20
Michael Clark
May 30, 2016, 5:56:56 AM5/30/16
to Jeremy, RISC-V SW Dev
There is also the CompCert C compiler to consider; which while it is Open Source; it is has a formal proof in Coq. It is a small C-only compiler (C99 with a few bits from C11). This is clearly much easier to prove than either Clang or GCC.
I have been reading the asm backends (it currently supports PowerPC, ARM and X86) and was surprised by some symmetry in the meta model (somewhat more sophisticated than our first attempt).
A CompCert RISC-V backend in Coq/OCaml would be an interesting project. I am not sure what certifications the CompCert compiler has and if there is a commercially validated version available.
From looking at the backends, a reasonable portion could be machine generated or derived from the ARM backend (which is of course more complex than RISC-V).
~mc
Sent from my iPhone
Sent from my iPhone
--
You received this message because you are subscribed to the Google Groups "RISC-V SW Dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to sw-dev+un...@groups.riscv.org.
To post to this group, send email to sw-...@groups.riscv.org.
Visit this group at https://groups.google.com/a/groups.riscv.org/group/sw-dev/.
To view this discussion on the web visit https://groups.google.com/a/groups.riscv.org/d/msgid/sw-dev/6862daee-8e99-44f3-b7a6-f13aa0506768%40groups.riscv.org.
Corey Richardson
May 30, 2016, 6:40:20 AM5/30/16
to Michael Clark, Jeremy, RISC-V SW Dev
On Mon, May 30, 2016 at 09:56:19PM +1200, Michael Clark wrote:
> There is also the CompCert C compiler to consider; which while it is Open
> Source; it is has a formal proof in Coq. It is a small C-only compiler (C99
> with a few bits from C11). This is clearly much easier to prove than either
> Clang or GCC.
>
> I have been reading the asm backends (it currently supports PowerPC, ARM and
> X86) and was surprised by some symmetry in the meta model (somewhat more
> sophisticated than our first attempt).
>
> A CompCert RISC-V backend in Coq/OCaml would be an interesting project. I am
> not sure what certifications the CompCert compiler has and if there is a
> commercially validated version available.
>
I'll note here that CakeML[0] already has a verified compiler which can target
> There is also the CompCert C compiler to consider; which while it is Open
> Source; it is has a formal proof in Coq. It is a small C-only compiler (C99
> with a few bits from C11). This is clearly much easier to prove than either
> Clang or GCC.
>
> I have been reading the asm backends (it currently supports PowerPC, ARM and
> X86) and was surprised by some symmetry in the meta model (somewhat more
> sophisticated than our first attempt).
>
> A CompCert RISC-V backend in Coq/OCaml would be an interesting project. I am
> not sure what certifications the CompCert compiler has and if there is a
> commercially validated version available.
>
RISC-V[1], using the L3 model of the ISA by SRI[2]. Their source language is,
right now, only an ML variant, but it's conceivable one could write a C
compiler to one of its intermediate representations (perhaps as an output of
CompCert - you'd get to use its C frontend and some of its optimizations. The
proofs don't quite compose like that (you'll need to trust (or verify
separately) that the translation is correct)).
[0] - https://cakeml.org/
[1] - https://github.com/CakeML/cakeml/blob/master/compiler/targets/riscv/riscv_targetScript.sml
[2] - https://github.com/SRI-CSL/l3riscv/blob/master/src/l3/riscv.spec
--
cmr
+610481782084
http://octayn.net/
Michael Clark
May 30, 2016, 9:58:15 AM5/30/16
to Corey Richardson, Jeremy, RISC-V SW Dev
CakeML looks interesting. I will definitely take a look when I have time.
As a side note, I find the general problem of testing a specification quite an interesting problem. Even with formal proofs there is the problem of proving something as true based on an erroneous assumption; in addition to the problem of human introduced transcription errors.
The comment earlier about dual compilers could also be applied to ISA interpreters. Spike and QEMU come to mind.
One considers the problem of a minimal JIT compiler for an ISA that is able to JIT itself from the ISA specification. This clearly emerges from a language that can describe the logic of the ISA in its most minimal form (we bootstrap from a shared language and notation).
My pragmatism (and following the lead set by riscv-opcodes) led me to remove almost all syntax altogether so we are only left with pure notation. This opens the door to expression in new languages that one can also use to derive the specification. English (or any other spoken language for that matter) seems to be boilerplate for the mind.
The security problem emerges from the semantic gap problem in that one has ambiguities in proving a barrier between privilege levels (*1). This extends beyond the ISA and the language of the system into the operating system kernel itself.
Randomisation (ASLR and the like) are merely shortcuts taken because the core security proof for the OS is missing. This leads my mind towards L4 in a ML with a JIT and a specification produced form the ML.
L4 for RISC-V in a ML might be an M5. There needs to be a tiny micro kernel that can turn declaration into execution (and we omit the complexity of synthesis into gate level logic). ~500 lines is quite an achievement (Z-Scale); only now we have an HDL and the need for symmetry with its notation.
http://ssrg.nicta.com.au/projects/TS/l4.verified/
The final point is really that one needs three implementations to prove one wrong (only to be left still suffering from the Byzantine general problem). Two only ensures dual consistency. Five is required to reduce the probability of one Byzantine general having less than 100% interest in maliciously crafted errors.
Seems we have diverged into full stack verification (ISA, compiler and OS) with 5 implementations of each.
UNIX, C and all of the associated security issues (buffer overflow, use-after free, double-free etc) emerged from an abstraction above PDP-11/20.
Is making a register distinguish between an address and a scalar a needless complexity? It seems one can only logically add a multiplied or divided displacement to an address to form another valid address (within some bounds). You can't shift an address but you can shift a scalar that you add to an address as a displacement. It never makes sense to add two addresses yet CPUs will do this happily. Would a secure processor ever make these kinds of distinctions at the register level? and fault if they saw an illegal operation (NaA - Not an Address symmetry with NaN). It seems there may be an 'address bit' which is orthogonal to a 'sign bit' for a scalar (this reminds me of the SORNs paper posted by Sam *2). The fatal flaw in current CPU designs that leads to vulnerabilities and errors is this lack of faults on operations that are legal for scalars but illegal for addresses (reflecting on history to prevent repeating its mistakes)
[1] "Best to keep it short"
[2] http://www.johngustafson.net/presentations/Multicore2016-JLG.pdf
~mc
Sent from my iPhone
As a side note, I find the general problem of testing a specification quite an interesting problem. Even with formal proofs there is the problem of proving something as true based on an erroneous assumption; in addition to the problem of human introduced transcription errors.
The comment earlier about dual compilers could also be applied to ISA interpreters. Spike and QEMU come to mind.
One considers the problem of a minimal JIT compiler for an ISA that is able to JIT itself from the ISA specification. This clearly emerges from a language that can describe the logic of the ISA in its most minimal form (we bootstrap from a shared language and notation).
My pragmatism (and following the lead set by riscv-opcodes) led me to remove almost all syntax altogether so we are only left with pure notation. This opens the door to expression in new languages that one can also use to derive the specification. English (or any other spoken language for that matter) seems to be boilerplate for the mind.
The security problem emerges from the semantic gap problem in that one has ambiguities in proving a barrier between privilege levels (*1). This extends beyond the ISA and the language of the system into the operating system kernel itself.
Randomisation (ASLR and the like) are merely shortcuts taken because the core security proof for the OS is missing. This leads my mind towards L4 in a ML with a JIT and a specification produced form the ML.
L4 for RISC-V in a ML might be an M5. There needs to be a tiny micro kernel that can turn declaration into execution (and we omit the complexity of synthesis into gate level logic). ~500 lines is quite an achievement (Z-Scale); only now we have an HDL and the need for symmetry with its notation.
http://ssrg.nicta.com.au/projects/TS/l4.verified/
The final point is really that one needs three implementations to prove one wrong (only to be left still suffering from the Byzantine general problem). Two only ensures dual consistency. Five is required to reduce the probability of one Byzantine general having less than 100% interest in maliciously crafted errors.
Seems we have diverged into full stack verification (ISA, compiler and OS) with 5 implementations of each.
UNIX, C and all of the associated security issues (buffer overflow, use-after free, double-free etc) emerged from an abstraction above PDP-11/20.
Is making a register distinguish between an address and a scalar a needless complexity? It seems one can only logically add a multiplied or divided displacement to an address to form another valid address (within some bounds). You can't shift an address but you can shift a scalar that you add to an address as a displacement. It never makes sense to add two addresses yet CPUs will do this happily. Would a secure processor ever make these kinds of distinctions at the register level? and fault if they saw an illegal operation (NaA - Not an Address symmetry with NaN). It seems there may be an 'address bit' which is orthogonal to a 'sign bit' for a scalar (this reminds me of the SORNs paper posted by Sam *2). The fatal flaw in current CPU designs that leads to vulnerabilities and errors is this lack of faults on operations that are legal for scalars but illegal for addresses (reflecting on history to prevent repeating its mistakes)
[1] "Best to keep it short"
[2] http://www.johngustafson.net/presentations/Multicore2016-JLG.pdf
~mc
Sent from my iPhone
Michael Clark
May 30, 2016, 10:04:11 AM5/30/16
to Corey Richardson, Jeremy, RISC-V SW Dev
Reducing the number of integer operations would allow us to reflect on what operations are valid on pairs of operands with or without address bits... Food for thought (it's not like there is not precedence in the FPU to add this sort of feature to the ALU). 65 bits?
Sent from my iPhone
Sent from my iPhone
> --
> You received this message because you are subscribed to the Google Groups "RISC-V SW Dev" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to sw-dev+un...@groups.riscv.org.
> To post to this group, send email to sw-...@groups.riscv.org.
> Visit this group at https://groups.google.com/a/groups.riscv.org/group/sw-dev/.
> To view this discussion on the web visit https://groups.google.com/a/groups.riscv.org/d/msgid/sw-dev/4ECF9BB9-9B34-43CE-97C0-2DAA04D3B10F%40mac.com.
> You received this message because you are subscribed to the Google Groups "RISC-V SW Dev" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to sw-dev+un...@groups.riscv.org.
> To post to this group, send email to sw-...@groups.riscv.org.
> Visit this group at https://groups.google.com/a/groups.riscv.org/group/sw-dev/.
Michael Clark
May 30, 2016, 11:00:47 AM5/30/16
to Corey Richardson, Jeremy, RISC-V SW Dev
64-bit is fine. it's not a bad idea. it's just more work. Address bit could be set on load and have additional precision in the register file much like the FPU register files on many CPUs. Loads would need 1 more bit to distinguish address load. Might be easy to fault based on a table of legal operations on registers with an address bit set? Sorry, thinking aloud.
Sent from my iPhone
> To view this discussion on the web visit https://groups.google.com/a/groups.riscv.org/d/msgid/sw-dev/2DC26D53-068B-4897-AFBE-8D2426785759%40mac.com.
Sent from my iPhone
Reply all
Reply to author
Forward
0 new messages