How do we make more open, secure and verifiable hardware?
RISC-V all the way down
I’m testing a shorter but bi-weekly cadence to keep things topical for a while. Feel free to give me feedback on twitter or mastodon at https://infosec.exchange/@prasincs
As we start 2023, I want to talk about the progress we are making in making secure hardware more open and verifiable.
Towards a More Secure Element Chip
I’m constantly surprised how much Bunnie Huang manages to do and have an impact on the security and hardware industry, not only does he have a pretty active presence on CrowdSupply, he’s also working with Cramium to build a more open supply to build a secure element
https://www.bunniestudios.com/blog/?p=6606
The summary here is that it’s still really hard to build a truly open Secure Element because a lot of technology is behind NDAs. This is a great illustration of where we are
I highly recommend reading the article itself because Bunnie is very realistic about the limitations of the approach here. This necessarily needs to be incremental because for the types of systems where these elements are used, the secrecy often may mean time to mitigate a truly critical vulnerability, something like “life and death” scenario. One can imagine many scenarios where vendors and users may be expected to handle this delicately.
As much as we want to build around Kerckhoff’s Principle aka standard assumption there was that serial number 1 of any new device was delivered to the Kremlin, there are practical engineering and market demand limitations mean that you need to make compromises. Fortunately we have made progress in fuzzing, tooling and formal systems, this could be key to solving a problem like this. I don’t yet know if this is a couple of years project or decades. Maybe we can incrementally keep proving parts of the system.
KataOS and Sparrow for RISC-V chips
This announcement tails very nicely to what I mean in previous news - incremental progress. Google announced a new operating system and framework for building low-power and secure embedded systems. It’s built on mathematically proven SeL4 but interestingly ignores the SeL4 kernel. I believe the kernel is provided by KataOS and CantripOS. To me this looks like a very logical incremental step, SeL4 has been well known in security circles and OpenTitan has been around for a while too. Writing it in Rust is also interesting choice. I really like the language, even though I have reservations on the ecosystem around it that I blogged on my Thoughts on Rust in 2023 post. Google is a pretty big user of Rust in their Fuchsia OS, notably it’s not allowed for frontend developers or the kernel according to their [policy on programming languages](https://fuchsia.dev/fuchsia-src/contribute/governance/policy/programming_languages#:~:text=Rust is not supported for,used in production operating systems.).
It’s available over here - I haven’t tried building it yet
https://github.com/AmbiML/sparrow-manifest
It seemed mostly incomplete for a passerby user like me
Internally, KataOS also is able to dynamically load and run third-party applications built outside of the CAmkES framework. At the moment, the code on Github does not include the required components to run these applications, but we hope to publish these features in the near future.
I’m expecting a paper at some point and 🤞for shipping this.
Aside: A Tour of the Fuchsia Operating System
I got really into Fuchsia in 2020 for a while and found it to be an interesting model. I came across this last year that really consolidated a lot of knowledge about the system - I recommend watching this talk if you’re curious how it works and how programming for it would look like.
On the next issue, I’ll talk about the progress made on https://www.zprize.io/ and brief analysis on the winning entry from Jane Street.