Skip to content

@secure-foundations Secure Foundations Lab

Change the repository type filter

All

    Repositories list

    37 repositories

    • vest

      Public
      High-assurance and performant Rust-based parsing and serialization of binary data formats verified in Verus
      Rust
      •
      MIT License
      •2•7•1•1•Updated Dec 23, 2024Dec 23, 2024

    • mariposa

      Public
      SMT
      •
      MIT License
      •7•11•5•0•Updated Dec 22, 2024Dec 22, 2024

    • owl

      Public
      Compositional Verification of Security Protocols
      Haskell
      •
      BSD 3-Clause "New" or "Revised" License
      •2•11•4•2•Updated Dec 17, 2024Dec 17, 2024

    • human-eval-verus

      Public
      Rust
      •
      MIT License
      •7•5•0•4•Updated Dec 12, 2024Dec 12, 2024

    • leaf

      Public
      Leaf library for Iris Concurrent Separation Logic
      Coq
      •
      Other
      •0•3•0•0•Updated Nov 27, 2024Nov 27, 2024

    • trie-hard

      Public
      Novel implementation of a Trie data structure optimized for small, sparse maps
      Rust
      •
      Apache License 2.0
      •11•0•0•0•Updated Oct 16, 2024Oct 16, 2024

    • ironsync-osdi2023

      Public
      IronSync paper artifact for OSDI 2023
      Dafny
      •
      Other
      •0•1•0•0•Updated Sep 8, 2024Sep 8, 2024

    • riptide-verification

      Public
      Python
      •0•1•0•0•Updated Aug 19, 2024Aug 19, 2024

    • veri-datalog

      Public
      Verified Datalog
      Dafny
      •2•5•0•0•Updated Aug 2, 2024Aug 2, 2024

    • axiom-profiler-2

      Public
      The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
      SMT
      •4•0•0•0•Updated Mar 26, 2024Mar 26, 2024

    • mariposa-data

      Public
      SMT
      •1•0•0•0•Updated Mar 21, 2024Mar 21, 2024

    • wabt-732

      Public
      The WebAssembly Binary Toolkit
      C++
      •
      Apache License 2.0
      •708•0•0•0•Updated Mar 20, 2024Mar 20, 2024

    • Mariposa-Ironclad

      Public
      The MSR Ironclad project builds provably secure and reliable systems.
      Dafny
      •
      Other
      •55•0•0•0•Updated Jan 23, 2024Jan 23, 2024

    • burrow

      Public
      Burrow coq formalization
      Coq
      •
      Other
      •0•1•0•0•Updated Jan 17, 2024Jan 17, 2024

    • rWasm

      Public
      A cross-platform high-performance provably-safe sandboxing Wasm-to-native compiler
      Rust
      •6•29•1•1•Updated Jan 14, 2024Jan 14, 2024

    • veri-titan

      Public
      Verifying OpenTitan
      Dafny
      •
      MIT License
      •3•23•1•0•Updated Aug 20, 2023Aug 20, 2023

    • mariposa-D_VBKV

      Public
      Dafny
      •2•0•0•0•Updated Jul 25, 2023Jul 25, 2023

    • dafny

      Public
      Dafny is a verification-aware programming language
      C#
      •
      Other
      •264•4•13•2•Updated Jul 6, 2023Jul 6, 2023

    • dafny-exercise

      Public
      Dafny
      •
      Other
      •0•0•0•0•Updated Mar 23, 2023Mar 23, 2023

    • SWISS

      Public
      Automatically synthesizing invariants of distributed systems
      Python
      •
      BSD 3-Clause "New" or "Revised" License
      •2•7•0•0•Updated Dec 1, 2022Dec 1, 2022

    • verifiable-computation

      Public
      Code for the Pinocchio and Geppetto Verifiable Computation systems
      F#
      •
      Other
      •0•5•0•0•Updated Oct 31, 2022Oct 31, 2022

    • iron-sync

      Public
      Iron Sync concurrent verification framework
      Dafny
      •
      Other
      •0•0•0•0•Updated Oct 25, 2022Oct 25, 2022

    • provably-safe-sandboxing-wasm-usenix22

      Public
      Top-level companion software artifact for the paper "Provably-Safe Multilingual Software Sandboxing using WebAssembly"
      WebAssembly
      •
      BSD 3-Clause "New" or "Revised" License
      •1•35•0•0•Updated Aug 30, 2022Aug 30, 2022

    • wasm-semantics-fuzzer

      Public
      An aid for developing correct WebAssembly implementations through generative fuzzing
      Rust
      •
      BSD 3-Clause "New" or "Revised" License
      •2•10•0•0•Updated Aug 30, 2022Aug 30, 2022

    • vWasm

      Public
      A formally-verified provably-safe sandboxing Wasm-to-native compiler
      OCaml
      •
      BSD 3-Clause "New" or "Revised" License
      •1•20•0•0•Updated Aug 30, 2022Aug 30, 2022

    • prettyplease

      Public
      fork of 'prettyplease' for verus
      Rust
      •
      Apache License 2.0
      •0•0•0•0•Updated Aug 20, 2022Aug 20, 2022

    • mariposa-D_KOMODO

      Public
      Formally-verified reference monitor for a secure isolated execution ("enclave") environment on ARM TrustZone
      C
      •
      Other
      •27•0•0•0•Updated Aug 18, 2022Aug 18, 2022

    • syn

      Public
      Parser for Rust source code
      Rust
      •
      Apache License 2.0
      •313•0•0•0•Updated Aug 17, 2022Aug 17, 2022

    • libraries

      Public
      Libraries useful for Dafny programs
      Dafny
      •
      Other
      •25•0•0•0•Updated Jan 28, 2022Jan 28, 2022

    • dafny_library

      Public archive
      Dafny
      •
      Other
      •0•0•0•0•Updated Oct 3, 2021Oct 3, 2021