2 ms·

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

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.

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.