Research
The group works on the software layer beneath modern hardware — operating systems, compilers, and runtimes — and on formal methods for reasoning about low-level code. Two directions are the key focus; several related threads run alongside them.
Verifying low-level software
A great deal of software exists only as binaries — stripped, optimized, without source code, and impossible to fully vouch for. This thrust builds the machinery to reason about such code with machine-checked guarantees. It begins by recovering the formal semantics of machine instructions automatically, rather than writing them by hand, and studies when disassembly is decidable at all. From there, position-independent binaries are lifted — verifiably — to symbolized assembly and to compiler intermediate representations, supported by binary-level pointer analysis and by the program logics and solvers that let the reasoning scale. On the resulting model, the group reasons about a class of security properties; the model can also be recompiled into a new binary that is provably equivalent to the original, subject to enumerated threats to validity. Verified patching — transforming the model and machine-checking that the change preserves correctness — is an ongoing direction. The soundness of each lifting phase, from disassembly onward, is formalized and proven.
Tools: LLRM · FoxDec · libLISA
Systems for heterogeneous-ISA hardware
Performance and energy-efficiency increasingly come from hardware that is harder to program: machines that mix instruction sets (e.g., x86 and Arm) and combine CPUs with FPGAs, SmartNICs, and RISC-V devices. This thrust builds operating systems, compilers, and runtimes — including a replicated-kernel operating system — that let a single application run and migrate across processors with different instruction sets. The work spans cross-ISA container migration, offloading long-running x86 workloads to low-power embedded (Arm) and RISC-V hardware, software diversification through instruction-set heterogeneity, cross-ISA process snapshotting, execution migration across FPGAs and CPUs, and resource borrowing across nodes, together with fused kernels for cache-coherent heterogeneous-ISA platforms, transparent cross-architecture enclave offloading, stateful CPU–FPGA migration, and software and hardware-based distributed shared-memory. A complementary line pursues a multiserver / library operating-system design.
Tools: Popcorn Linux · LibrettOS
Related directions
On the security of existing software, the group builds tools to find and reach vulnerabilities — generating fuzzing harnesses, instrumenting binaries for sanitization and coverage, and fuzzing libraries and protocols — and lifts binaries to compiler IR to support such analysis. Safely modernizing legacy code is a growing thread, including automated translation of C into memory-safe Rust that targets freedom from known vulnerabilities and from memory leaks and undefined behavior.
Further work spans new program-analysis techniques and scalable satisfiability solvers, low-level (microcode) reprogramming of processors, and root-cause analysis for fuzzing and program superoptimization. This work draws on the group's roots in concurrency, distributed systems, operating systems, and real-time computing.