4 ms·

One area that I have been exploring is building equivalence proofs between high-level specifications, an implementation in C, and the machine code output from t

One area that I have been exploring is building equivalence proofs between high-level specifications, an implementation in C, and the machine code output from the compiler. I'm still very early in that work, but one of my hopes is to at least demonstrate that the output still meets the specifications, and that we can control things like timing (e.g. no branching on secret data) and cache in this output. I think that the compilation and optimization step, as a black box, is a disservice for highly reliable software development. Compiler and optimizer bugs are definitely a thing. I was bitten by one that injected timing attacks into certain integer operations by branching on the integer data in order to optimize 32-bit multiplications on 8-bit microcontrollers. Yeah, this makes perfect sense when trying to optimize fixed point multiplication, but it completely destroys the security of DLP or ecDLP based cryptography by introducing timing attacks that can recover the private key. Thankfully, I was fastidious about examining the optimized machine code output of this compiler, and was able to substitute hand coded assembler in its place.

cesarb 2y ago
> One area that I have been exploring is building equivalence proofs between high-level specifications, an implementation in C, and the machine code output from the compiler. AFAIK, that's how seL4 is verified. Quoting from https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html#what-does-sel4s-formal-verification-mean https://docs.sel4.systems/projects/sel4/frequently-asked-que... "[...] Specifically, the ARM, ARM_HYP (ARM with virtualisation extensions), X64, and RISCV64 versions of seL4 comprise the first (and still only) general-purpose OS kernel with a full code-level functional correctness proof, meaning a mathematical proof that the implementation (written in C) adheres to its specification. [...] On the ARM and RISCV64 platforms, there is a further proof that the binary code which executes on the hardware is a correct translation of the C code. This means that the compiler does not have to be trusted, and extends the functional correctness property to the binary. [...] Combined with the proofs mentioned above, these properties are guaranteed to be enforced not only by a model of the kernel (the specification) but the actual binary that executes on the hardware."
- nanolith 2y ago
  Indeed it is. What I'm working toward is a more efficient way to do the same, that doesn't take the touted 30 man years of effort to accomplish. I'm working on a hybrid approach between SMT solving and constructive proofs. Model checking done with an SMT solver is pretty sound. I'm actually planning a book on a scalable technique to do this with CBMC. But, the last leg of this really is understanding the compiler output.
gizmo686 2y ago
If you haven't done so, you might want to look at some of the work done by the seL4 microkernel project. They start with a Haskell prototype that is translated programatically into a formal specification for the theorem prover. They then implement the same thing in C, and use a refinement prove to demonstrate that it matches their Haskell implementation. They then compile the program, and create another refinement proof to demonstrate that the binary code matches the C semantics.
- nanolith 2y ago
  I'll refer you to my reply to a sibling comment. I'm hoping that I can build a more efficient means of doing similar work as with seL4, but without the 30 man year effort. They are on the right track. But, I think there have been some improvements since their effort that can lead to more streamlined equivalence proofs.
nlewycky 2y ago
> I was bitten by one that injected timing attacks into certain integer operations by branching on the integer data in order to optimize 32-bit multiplications on 8-bit microcontrollers. FWIW, I think this should be considered a language design problem rather than an optimizer design problem. Black box optimizer behaviour is good for enabling language designs that have little connection to hardware behaviour, and good for portability including to different extensions within an ISA. C doesn't offer a way to express any timing guarantees. The compiler, OS, CPU designer, etc. can't even do the right thing if they wanted to because the necessary information isn't being received from the programmer.
- jcranmer 2y ago
  To a large degree, constant-time programming is hampered by the fact that even hardware is often unwilling to provide constant-time guarantees, let alone any guarantees that the compiler would care to preserve. (Although, to be honest, constant-time guarantees are the sort of things that most compiler writers prefer to explicitly not guarantee in any circumstances whatsoever).
  - bluGill 2y ago
    8 bit cpus offer constant time. 16 bit was starting to get into the issues where you cannot off it.
    - wiml 2y ago
      Your comment makes me wonder about the idea of building a superscalar, out of order, speculative implementation of the 6502 or 8080 instruction sets. Might make a good educational project.
  - yxhuvud 2y ago
    If it were starting to show up in languages though, then that would make it more likely for hardware to start introducing functionality like this.
- nanolith 2y ago
kragen 2y ago
What do you think about Jasmin?
- nanolith 2y ago
  Jasmin has some great ideas. My goal in particular is to improve the tooling around C so that verification of C programs is easier. Because there are trillions of lines of C out there, I want to ensure that semi-automated processes can be developed for verifying and fixing this code. For cryptography, this involves similar features as Jasmin. The main difference is that I'm looking at ways to guide this while largely preserving the C language. That's not because I think C is better, but because I want to inject this into existing code bases and development processes, with existing software developers.
  - kragen 2y ago
    It sounds like a very promising approach! Do you think there are really trillions of lines of C? At ten delivered and debugged lines of code per programmer-day we'd have on the order of a single trillion lines ever written, but most of that has been discarded, and probably less than half of the remainder is C. I suspect something like wasm may be a better way to preserve backward-compatibility with C, although of course it won't help with constant time or confused-deputy vulnerabilities. CHERI might help with the latter.
    - nanolith 2y ago
      That's based on current estimates. It's impossible to know for certain, but there is a lot of C software out there. I'm a big fan of runtime mitigations. I use a few in my own work. WASM can help in some areas. But, bear in mind that a lot of this C source code is firmware or lower level operating system details (e.g. kernels, device drivers, system services, low-level APIs, portable cryptography routines). In this case, WASM wouldn't be a good fit. CHERI is also a possibility in some contexts for runtime mitigation. But, since that does involve a hardware component, unless or until such capabilities are available in mainstream devices and microcontrollers, this would only be of limited use. There are other runtime mitigations that are more mainstream, such as pointer authentication, that are in various states of evaluation, deployment, or regression due to hardware vulnerabilities. I think that each of these runtime mitigations are important for defense in depth, but I think that defense in depth works best when these mitigations are adding an additional layer of protection instead of the only layer of protection. So, this verification work should be seen as an added layer of protection on top of runtime mitigations, which I hope will become more widely available as time goes on.

cesarb 2y ago

> One area that I have been exploring is building equivalence proofs between high-level specifications, an implementation in C, and the machine code output from the compiler. AFAIK, that's how seL4 is verified. Quoting from https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html#what-does-sel4s-formal-verification-mean https://docs.sel4.systems/projects/sel4/frequently-asked-que... "[...] Specifically, the ARM, ARM_HYP (ARM with virtualisation extensions), X64, and RISCV64 versions of seL4 comprise the first (and still only) general-purpose OS kernel with a full code-level functional correctness proof, meaning a mathematical proof that the implementation (written in C) adheres to its specification. [...] On the ARM and RISCV64 platforms, there is a further proof that the binary code which executes on the hardware is a correct translation of the C code. This means that the compiler does not have to be trusted, and extends the functional correctness property to the binary. [...] Combined with the proofs mentioned above, these properties are guaranteed to be enforced not only by a model of the kernel (the specification) but the actual binary that executes on the hardware."

nanolith 2y ago
Indeed it is. What I'm working toward is a more efficient way to do the same, that doesn't take the touted 30 man years of effort to accomplish. I'm working on a hybrid approach between SMT solving and constructive proofs. Model checking done with an SMT solver is pretty sound. I'm actually planning a book on a scalable technique to do this with CBMC. But, the last leg of this really is understanding the compiler output.

gizmo686 2y ago

If you haven't done so, you might want to look at some of the work done by the seL4 microkernel project. They start with a Haskell prototype that is translated programatically into a formal specification for the theorem prover. They then implement the same thing in C, and use a refinement prove to demonstrate that it matches their Haskell implementation. They then compile the program, and create another refinement proof to demonstrate that the binary code matches the C semantics.

nanolith 2y ago
I'll refer you to my reply to a sibling comment. I'm hoping that I can build a more efficient means of doing similar work as with seL4, but without the 30 man year effort. They are on the right track. But, I think there have been some improvements since their effort that can lead to more streamlined equivalence proofs.

nlewycky 2y ago

> I was bitten by one that injected timing attacks into certain integer operations by branching on the integer data in order to optimize 32-bit multiplications on 8-bit microcontrollers. FWIW, I think this should be considered a language design problem rather than an optimizer design problem. Black box optimizer behaviour is good for enabling language designs that have little connection to hardware behaviour, and good for portability including to different extensions within an ISA. C doesn't offer a way to express any timing guarantees. The compiler, OS, CPU designer, etc. can't even do the right thing if they wanted to because the necessary information isn't being received from the programmer.

jcranmer 2y ago
To a large degree, constant-time programming is hampered by the fact that even hardware is often unwilling to provide constant-time guarantees, let alone any guarantees that the compiler would care to preserve. (Although, to be honest, constant-time guarantees are the sort of things that most compiler writers prefer to explicitly not guarantee in any circumstances whatsoever).
- bluGill 2y ago
  8 bit cpus offer constant time. 16 bit was starting to get into the issues where you cannot off it.
  - wiml 2y ago
    Your comment makes me wonder about the idea of building a superscalar, out of order, speculative implementation of the 6502 or 8080 instruction sets. Might make a good educational project.
- yxhuvud 2y ago
  If it were starting to show up in languages though, then that would make it more likely for hardware to start introducing functionality like this.
nanolith 2y ago

kragen 2y ago

What do you think about Jasmin?

nanolith 2y ago
Jasmin has some great ideas. My goal in particular is to improve the tooling around C so that verification of C programs is easier. Because there are trillions of lines of C out there, I want to ensure that semi-automated processes can be developed for verifying and fixing this code. For cryptography, this involves similar features as Jasmin. The main difference is that I'm looking at ways to guide this while largely preserving the C language. That's not because I think C is better, but because I want to inject this into existing code bases and development processes, with existing software developers.
- kragen 2y ago
  It sounds like a very promising approach! Do you think there are really trillions of lines of C? At ten delivered and debugged lines of code per programmer-day we'd have on the order of a single trillion lines ever written, but most of that has been discarded, and probably less than half of the remainder is C. I suspect something like wasm may be a better way to preserve backward-compatibility with C, although of course it won't help with constant time or confused-deputy vulnerabilities. CHERI might help with the latter.
  - nanolith 2y ago
    That's based on current estimates. It's impossible to know for certain, but there is a lot of C software out there. I'm a big fan of runtime mitigations. I use a few in my own work. WASM can help in some areas. But, bear in mind that a lot of this C source code is firmware or lower level operating system details (e.g. kernels, device drivers, system services, low-level APIs, portable cryptography routines). In this case, WASM wouldn't be a good fit. CHERI is also a possibility in some contexts for runtime mitigation. But, since that does involve a hardware component, unless or until such capabilities are available in mainstream devices and microcontrollers, this would only be of limited use. There are other runtime mitigations that are more mainstream, such as pointer authentication, that are in various states of evaluation, deployment, or regression due to hardware vulnerabilities. I think that each of these runtime mitigations are important for defense in depth, but I think that defense in depth works best when these mitigations are adding an additional layer of protection instead of the only layer of protection. So, this verification work should be seen as an added layer of protection on top of runtime mitigations, which I hope will become more widely available as time goes on.