Secure Foundations Lab
We investigate long-term, fundamental improvements in how to design and build secure systems.
Pinned Repositories
human-eval-verus
mariposa
owl
Compositional Verification of Security Protocols
provably-safe-sandboxing-wasm-usenix22
Top-level companion software artifact for the paper "Provably-Safe Multilingual Software Sandboxing using WebAssembly"
rWasm
A cross-platform high-performance provably-safe sandboxing Wasm-to-native compiler
veri-titan
Verifying OpenTitan
veribetrkv-osdi2020
VeriBetrKV OSDI'20 artifact
vest
High-assurance and performant Rust-based parsing and serialization of binary data formats verified in Verus
vWasm
A formally-verified provably-safe sandboxing Wasm-to-native compiler
wasm-semantics-fuzzer
An aid for developing correct WebAssembly implementations through generative fuzzing
Secure Foundations Lab's Repositories
secure-foundations/provably-safe-sandboxing-wasm-usenix22
Top-level companion software artifact for the paper "Provably-Safe Multilingual Software Sandboxing using WebAssembly"
secure-foundations/rWasm
A cross-platform high-performance provably-safe sandboxing Wasm-to-native compiler
secure-foundations/veri-titan
Verifying OpenTitan
secure-foundations/vWasm
A formally-verified provably-safe sandboxing Wasm-to-native compiler
secure-foundations/mariposa
secure-foundations/human-eval-verus
secure-foundations/wasm-semantics-fuzzer
An aid for developing correct WebAssembly implementations through generative fuzzing
secure-foundations/owl
Compositional Verification of Security Protocols
secure-foundations/vest
High-assurance and performant Rust-based parsing and serialization of binary data formats verified in Verus
secure-foundations/SWISS
Automatically synthesizing invariants of distributed systems
secure-foundations/veri-datalog
Verified Datalog
secure-foundations/verifiable-computation
Code for the Pinocchio and Geppetto Verifiable Computation systems
secure-foundations/dafny
Dafny is a verification-aware programming language
secure-foundations/leaf
Leaf library for Iris Concurrent Separation Logic
secure-foundations/riptide-verification
secure-foundations/burrow
Burrow coq formalization
secure-foundations/ironsync-osdi2023
IronSync paper artifact for OSDI 2023
secure-foundations/axiom-profiler-2
The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
secure-foundations/dafny-exercise
secure-foundations/dafny_library
secure-foundations/iron-sync
Iron Sync concurrent verification framework
secure-foundations/libraries
Libraries useful for Dafny programs
secure-foundations/mariposa-D_KOMODO
Formally-verified reference monitor for a secure isolated execution ("enclave") environment on ARM TrustZone
secure-foundations/mariposa-D_VBKV
secure-foundations/mariposa-data
secure-foundations/Mariposa-Ironclad
The MSR Ironclad project builds provably secure and reliable systems.
secure-foundations/prettyplease
fork of 'prettyplease' for verus
secure-foundations/syn
Parser for Rust source code
secure-foundations/trie-hard
Novel implementation of a Trie data structure optimized for small, sparse maps
secure-foundations/wabt-732
The WebAssembly Binary Toolkit