4 ms·

I think you would also have to verify resulting binary, compiler, libraries... It seems more manageable to verify a few KB of assembly or C

by jkot 10y ago

pjmlp 10y ago
Not really, to verify C code you need to set the compiler and its corresponding version in stone for the verification process, as UB can change even between versions of the same compiler.
- cmrx64 10y ago
  Not really true. See https://www.nicta.com.au/publications/research-publications/?pid=6449 https://www.nicta.com.au/publications/research-publications/... for how the compiler and its internal semantics are completely removed from the chain for l4v.
  - pjmlp 10y ago
    Thanks for the link, I will have a look into it.
nickpsecurity 10y ago
It would seem but it's actually the opposite with existing tooling thanks to COGENT. Amateurs did a filesystem with a fraction of the work that pro's did the kernel: https://ts.data61.csiro.au/projects/TS/cogent.pml https://ts.data61.csiro.au/projects/TS/cogent.pml Note: See "Cogent: Verifying high-assurance file system..." They leverage the same tools used for seL4 verification. Also worth noting that Myreen et al's toolkit basically converts HOL specifications to machine code without need for an external compiler. The "C" that was compiled was an embedding of it in HOL called Simpl which the aforementioned process verifies and converts to verified code. This is called translation validation. That's my non-specialist understanding of what the papers said. COGENT builds on this process to convert functional language and easier specs into that form which gets trans-validated into machine code. With less effort. :) Note: Myreen et al are doing both verifications of HOL itself and HOL to hardware translation next. These further reduce the TCB of provers and hardware respectively to almost nothing but the specs.
felixk42 10y ago
Exactly, and then one has to deal with the runtime and GC.

I think you would also have to verify resulting binary, compiler, libraries... It seems more manageable to verify a few KB of assembly or C

by jkot 10y ago

I think you would also have to verify resulting binary, compiler, libraries... It seems more manageable to verify a few KB of assembly or C

pjmlp 10y ago

Not really, to verify C code you need to set the compiler and its corresponding version in stone for the verification process, as UB can change even between versions of the same compiler.

cmrx64 10y ago
Not really true. See https://www.nicta.com.au/publications/research-publications/?pid=6449 https://www.nicta.com.au/publications/research-publications/... for how the compiler and its internal semantics are completely removed from the chain for l4v.
- pjmlp 10y ago
  Thanks for the link, I will have a look into it.

nickpsecurity 10y ago

It would seem but it's actually the opposite with existing tooling thanks to COGENT. Amateurs did a filesystem with a fraction of the work that pro's did the kernel: https://ts.data61.csiro.au/projects/TS/cogent.pml https://ts.data61.csiro.au/projects/TS/cogent.pml Note: See "Cogent: Verifying high-assurance file system..." They leverage the same tools used for seL4 verification. Also worth noting that Myreen et al's toolkit basically converts HOL specifications to machine code without need for an external compiler. The "C" that was compiled was an embedding of it in HOL called Simpl which the aforementioned process verifies and converts to verified code. This is called translation validation. That's my non-specialist understanding of what the papers said. COGENT builds on this process to convert functional language and easier specs into that form which gets trans-validated into machine code. With less effort. :) Note: Myreen et al are doing both verifications of HOL itself and HOL to hardware translation next. These further reduce the TCB of provers and hardware respectively to almost nothing but the specs.

felixk42 10y ago

Exactly, and then one has to deal with the runtime and GC.