operating systems

Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications
This paper presents a mechanized formal semantics for the Linux eBPF instruction set architecture (ISA). We develop a small-step …
Cite
Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications
Formal Specification of Linux eBPF Instruction Set Architecture in Sail
eBPF has become a widely-used mechanism for extending the Linux kernel, and recent standardization efforts have produced the first …
Cite
Formal Specification of Linux eBPF Instruction Set Architecture in Sail
PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot under Hardware Supply-chain Attacks
Hardware supply-chain attacks are raising significant security threats to the boot process of multiprocessor systems. In this paper, we …
PDF Cite DOI
PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot under Hardware Supply-chain Attacks