There's an SBIR I'd like to apply to, but it'd be helpful to have a team when proposing. My current employer is open to applying to SBIRs outside of their current domain of expertise, and is currently registered to be able to do contracts with the government.

I know that people have read my blog in the past, so I'm hoping to find the following types of folks interested in working on the SBIR(which I'll elaborate on later in this post).

In particular, I'm hoping to find folks with at least one of the following qualifications:

• experience with Clash-Haskell, or even just Haskell
• experience with CPU design
• experience with DDR controller and or PCI-e controller design
• meaningful exposure to formal methods
• experience/expertise in the seL4 kernel

The SBIR has some issues in its current state, but it's not uncommon for an offeror on an SBIR to refine the topic towards a more useful direction. I put forward some thoughts on what I think such a direction could look like towards the end of this post.

The SBIR in its Current State

This is the SBIR I encountered, which is looking for contractors interested in reducing the attack surface of the seL4 kernel(RISC-V variant) by:

1. Removing/reducing the amount of assembly code the in the seL4 kernel.
2. Implementing a RISC-V softcore that supports the modified seL4 kernel.

The SBIR references some literature on moving OS primitives into hardware as well as literature reinforcing the fact that RISC-V is extensible.

Nevertheless, the SBIR as proposed doesn't make much sense to me for the following reasons:

1. I've had a chance to take a brief look through some of the seL4 inline assembly portions, and they're what I'd consider to be minimal or nearly minimal, namely, register saving code, trap code, and SMP code.
2. The sel4 kernel gets compiled to assembly anyway.
3. It seems some of the concepts mentioned in the rather old literature the SBIR mentions have evolved into the following modern hardware concepts:
   • MMUs
   • TLBs
   • permission bits in memory pages - often part of the MMUs domain
   • atomic memory operations
   • hypervisors
   • secure enclaves
4. The concepts in the literature the SBIR references don't seem to map well to sel4, for example:
   • Nakano's paper is mainly oriented toward RTOSs, and specifically deals with implementing a task scheduler in hardware. seL4 isn't exactly an RTOS.
   • Intel's iAPX 432 was neither a technical nor commercial success. It focused on implementing primitives that would help speed up execution of Ada code. seL4 however is written in C, which, unlike Ada, is a language designed to be a minimal wrapper above assembly - and in a sense, modern processors are already optimized to run C.
   • The Higher order software paper uses terminology that is a bit antiquated(1977), but by briefly reviewing that paper, I was able to surmise that the authors were searching for OS-supporting hardware primitives that the modern industry has already converged on.

A Better Question

Instead, it seems to me that the fundamental concern motivating this SBIR is whether or not we can trust the hardware on which seL4 executes, which is a completely valid question to ask, a question to which I'd respond - probably not.

My estimate of what would constitute a trustworthy computational substrate would be comprised of the following:

• formally verified CPU - could include verification of:
  • the re-order buffer, ensuring causality is preserved under certain conditions and over certain windows of time
  • cache coherency
• open source DDR and PCI-e controller with open firmware that is formally proven to be non-malicious where non-malicious is well defined. Note that a compromised DDR or PCI-e controller can easily lie to the CPU about content at a certain address.
• formally verified graph rewrite portion of the synthesis toolchain

I think an interesting approach would involve designing the CPU in Clash-Haskell and then using Liquid-Haskell, Agda, or Coq for formal verification.

Here is an interesting paper discussing the potential of proof by type-refinement on a Clash-Haskell hardware design.

Re-Directing The SBIR

My current employer has experience working on SBIRs whose original problem statements weren't well-formed. To address this, it is possible to intentionally steer the SBIR in a useful direction in the early contract stages.

To have a good chance at winning this SBIR would require a multi-disciplinary team likely comprised of some seL4 as well as hardware expertise.

If working on this SBIR sounds interesting to you, and you have one or more of the qualifications I listed at the beginning of this post, or even if you just have some helpful remarks, please reach out to me at: yehowshua.immanuel@radialrad.com.

Some of My Work

For your reference, I currently work in a completely unrelated area full-time, but have worked on the following in the past, some of which I still work on in my spare time:

1. A PowerPC CPU design I did a little bit of work on in SpinalHDL(a language like Scala-Chisel) in 2021.

2. A high performance VCD parser written in Rust in 2022, that I've mostly stopped working on as I've realized that doing hardware design in Haskell doesn't really require a VCD viewer.

   Nevertheless, theZoq has been working on a VCDViewer graphical frontend the builds on top of the VCD parser I wrote.

3. Some small experiments in Haskell-Clash targeting the ULX3S FPGA.

4. Some work on bringing Bluespec's documentation online, out of the search-engine unfriendly PDF format.