Hi, my name is Carson. I’m currently an undergrad at Northwestern studying math and computer science. I work in the Prescience Lab, led by Professor Peter Dinda. My main research interests are operating system microkernels, hardware/software formal verification, cryptography, and homotopy type theory.

I’m an active contributor to the following projects:

• Constellation: full software and hardware stack for frictionless heterogeneous parallelism

• Privacy Backplane: enabling individualized privacy policies in IoT environments, such as cashierless stores

• CARAT KOP: memory guards for Linux kernel modules. A paper on this topic was accepted to ROSS 2023 as of September 8th, 2023.

• BEANDIP: using dispersed interrupt polling to replace hardware interrupts. A related work I’m working on is applying the Green-Tao theorem to prevent against timing-related side-channel attacks.

• Village: compiler for NESL/VCODE to LLVM-IR. My current work is adding exception support to RISC-V Vector Extensions in the BOOM/Ocelot core; significant portions of BOOM written in Verilog are being converted to verified Chisel through ChiselVerify. A portion of this work is done at Sandia National Lab.

• Tortoise (Creator): Peer-to-Peer network for Privacy Backplane using libp2p

• WASMwand (Creator): a WASM runtime with some deterministic magic. Built around a novel HoTT and category theory based approach to formalizing the WASM runtime and WASM-to-kernel interfaces.

  There are many subprojects to WASMwand. Notable ones include:

  • Formal Syscall Spec: formalized descriptions on how a kernel should complete common syscall operations, written in Lean 4.

  • Nimue: ephemeral hypervisors for deductive kernel verification.

  • Reynard: a capability-based, library operating system for creating unikernels.

  • Ice V: a collection of tools for deploying formally verified RISC-V cores on AWS F1 instances.

Notable previous work:

• Nautilus Microkernel, completing both a RISC-V port and ARMv8 port.

• TrackFM: a transparent, and user level, far memory management system, developed at Hexsa Lab in IIT.

• VirGL

• BcacheFS

• KVM

I’m highly proficient in the Rust, C, Python, Bash, and awk languages. I have high familiarity with and am actively learning Lean, Scala/Chisel HDL and Verilog. I also work on open-source maintenance on a variety of smaller projects. In my free time I like working on VR/AR/wearable hardware and improving my homelab.

If you’re interested in working on something together, contact me at carson@surmeier.us