Skip to content
Change the repository type filter

All

    Repositories list

    • am-cakeml

      Public
      Delivery repo for the KU CakeML Attestation Manager
      Standard ML
      GNU General Public License v3.0
      1111Updated Jan 7, 2025Jan 7, 2025
    • Copland Attestation Virtual Machine definition and tools
      Coq
      3390Updated Jan 6, 2025Jan 6, 2025
    • asp-libs

      Public
      Repository for implementations of attestation service provider (asp) libraries (libs).
      C
      2000Updated Jan 6, 2025Jan 6, 2025
    • bib

      Public
      TeX
      0000Updated Jan 2, 2025Jan 2, 2025
    • llncs-template

      Public template
      Template for creating a repo for an llncs-style paper with our BibTeX files, includes, natbib, and headers in place.
      TeX
      1000Updated Dec 20, 2024Dec 20, 2024
    • Thoughts on interfacing RESOLUTE and Copland
      Coq
      00160Updated Dec 20, 2024Dec 20, 2024
    • coq-template

      Public template
      Template file for a new Coq project
      Makefile
      Creative Commons Attribution Share Alike 4.0 International
      0000Updated Dec 13, 2024Dec 13, 2024
    • A repository to hold Rust crates and common libraries that support building Copland ASPs and AMs (Attestation Managers) in Rust
      Rust
      0000Updated Dec 9, 2024Dec 9, 2024
    • CakeML semantics in Coq
      Coq
      1000Updated Dec 4, 2024Dec 4, 2024
    • Formal synthesis of CakeML from Coq functions
      Coq
      Creative Commons Attribution Share Alike 4.0 International
      0000Updated Oct 31, 2024Oct 31, 2024
    • SLDG Webpage
      CSS
      0000Updated Oct 21, 2024Oct 21, 2024
    • coq

      Public
      Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
      OCaml
      GNU Lesser General Public License v2.1
      661000Updated Sep 24, 2024Sep 24, 2024
    • HTML
      0050Updated Sep 17, 2024Sep 17, 2024
    • A repository for attestation manager (am) client implementations.
      Rust
      0000Updated Sep 3, 2024Sep 3, 2024
    • copland

      Public
      All things related to the Copland attestation protocol language and its derivatives.
      1010Updated Aug 23, 2024Aug 23, 2024
    • Test repo
      Makefile
      0000Updated Jul 15, 2024Jul 15, 2024
    • attarch

      Public
      Attestation Architecture
      C
      BSD 3-Clause "New" or "Revised" License
      0000Updated Jul 11, 2024Jul 11, 2024
    • Attestation Architecture manifest
      BSD 3-Clause "New" or "Revised" License
      0000Updated Jun 19, 2024Jun 19, 2024
    • BSD 3-Clause "New" or "Revised" License
      00110Updated Jun 17, 2024Jun 17, 2024
    • coq2rust

      Public
      Synthesis of Rust from Coq specifications
      BSD 3-Clause "New" or "Revised" License
      0030Updated May 28, 2024May 28, 2024
    • fm24

      Public
      Submission to FM'24
      TeX
      0000Updated Apr 26, 2024Apr 26, 2024
    • Musings about how we might make run-time measurement more effective and automatic.
      TeX
      0000Updated Feb 9, 2024Feb 9, 2024
    • Coq
      0050Updated Jan 22, 2024Jan 22, 2024
    • Haskell Attestation Manager implementation and tools
      Haskell
      BSD 3-Clause "New" or "Revised" License
      0100Updated Dec 19, 2023Dec 19, 2023
    • nfm24

      Public
      Repo for paper on TPM key certification verification
      TeX
      0000Updated Dec 15, 2023Dec 15, 2023
    • A common place for sharing Coq examples to support discussions in the lab.
      Coq
      0000Updated Nov 21, 2023Nov 21, 2023
    • plih

      Public
      Programming Languages in Haskell support documents
      Haskell
      BSD 3-Clause "New" or "Revised" License
      0000Updated Aug 24, 2023Aug 24, 2023
    • Bisimulation Theories
      Coq
      BSD 2-Clause "Simplified" License
      0000Updated Aug 9, 2023Aug 9, 2023
    • vstte23

      Public
      Repo for paper on TPM key certification verification
      TeX
      0000Updated Aug 4, 2023Aug 4, 2023
    • Implementation of a JSON interface to the Copland Virtual Machine (CVM) and Copland Appraisal Procedure (CAP). Also a proof of concept client application that prepares inputs, exercises the interfaces, outputs results.
      GNU General Public License v3.0
      0000Updated Jun 2, 2023Jun 2, 2023
    51 repositories found. List is sorted by Last pushed in descending order.