Repositories list

• am-cakeml

  Public
  Delivery repo for the KU CakeML Attestation Manager

  Standard ML

  •

  GNU General Public License v3.0

  •1•1•1•1•Updated Jan 8, 2025Jan 8, 2025

• copland-avm

  Public
  Copland Attestation Virtual Machine definition and tools

  Coq

  •3•3•9•0•Updated Jan 6, 2025Jan 6, 2025

• asp-libs

  Public
  Repository for implementations of attestation service provider (asp) libraries (libs).

  C

  •2•0•0•0•Updated Jan 6, 2025Jan 6, 2025

• bib

  Public
  TeX

  •0•0•0•0•Updated 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

  •1•0•0•0•Updated Dec 20, 2024Dec 20, 2024

• resolute-copland

  Public
  Thoughts on interfacing RESOLUTE and Copland

  Coq

  •0•0•16•0•Updated 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

  •0•0•0•0•Updated Dec 13, 2024Dec 13, 2024

• rust-am-lib

  Public
  A repository to hold Rust crates and common libraries that support building Copland ASPs and AMs (Attestation Managers) in Rust

  Rust

  •0•0•0•0•Updated Dec 9, 2024Dec 9, 2024

• cakeml-coq

  Public
  CakeML semantics in Coq

  Coq

  •1•0•0•0•Updated Dec 4, 2024Dec 4, 2024

• coq2cakeml

  Public
  Formal synthesis of CakeML from Coq functions

  Coq

  •

  Creative Commons Attribution Share Alike 4.0 International

  •0•0•0•0•Updated Oct 31, 2024Oct 31, 2024

• ku-sldg.github.io

  Public
  SLDG Webpage

  CSS

  •0•0•0•0•Updated 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

  •661•0•0•0•Updated Sep 24, 2024Sep 24, 2024

• protocol_ordering

  Public
  HTML

  •0•0•5•0•Updated Sep 17, 2024Sep 17, 2024

• am-clients

  Public
  A repository for attestation manager (am) client implementations.

  Rust

  •0•0•0•0•Updated Sep 3, 2024Sep 3, 2024

• copland

  Public
  All things related to the Copland attestation protocol language and its derivatives.

  1•0•1•0•Updated Aug 23, 2024Aug 23, 2024

• workflow_testing

  Public
  Test repo

  Makefile

  •0•0•0•0•Updated Jul 15, 2024Jul 15, 2024

• attarch

  Public
  Attestation Architecture

  C

  •

  BSD 3-Clause "New" or "Revised" License

  •0•0•0•0•Updated Jul 11, 2024Jul 11, 2024

• attarch-manifest

  Public
  Attestation Architecture manifest

  BSD 3-Clause "New" or "Revised" License

  •0•0•0•0•Updated Jun 19, 2024Jun 19, 2024

• attestation-testbed

  Public
  BSD 3-Clause "New" or "Revised" License

  •0•0•11•0•Updated Jun 17, 2024Jun 17, 2024

• coq2rust

  Public
  Synthesis of Rust from Coq specifications

  BSD 3-Clause "New" or "Revised" License

  •0•0•3•0•Updated May 28, 2024May 28, 2024

• fm24

  Public
  Submission to FM'24

  TeX

  •0•0•0•0•Updated Apr 26, 2024Apr 26, 2024

• measurement22

  Public
  Musings about how we might make run-time measurement more effective and automatic.

  TeX

  •0•0•0•0•Updated Feb 9, 2024Feb 9, 2024

• negotiation20

  Public
  Coq

  •0•0•5•0•Updated Jan 22, 2024Jan 22, 2024

• haskell-am

  Public
  Haskell Attestation Manager implementation and tools

  Haskell

  •

  BSD 3-Clause "New" or "Revised" License

  •0•1•0•0•Updated Dec 19, 2023Dec 19, 2023

• nfm24

  Public
  Repo for paper on TPM key certification verification

  TeX

  •0•0•0•0•Updated Dec 15, 2023Dec 15, 2023

• coqMusings

  Public
  A common place for sharing Coq examples to support discussions in the lab.

  Coq

  •0•0•0•0•Updated Nov 21, 2023Nov 21, 2023

• plih

  Public
  Programming Languages in Haskell support documents

  Haskell

  •

  BSD 3-Clause "New" or "Revised" License

  •0•0•0•0•Updated Aug 24, 2023Aug 24, 2023

• simulation

  Public
  Bisimulation Theories

  Coq

  •

  BSD 2-Clause "Simplified" License

  •0•0•0•0•Updated Aug 9, 2023Aug 9, 2023

• vstte23

  Public
  Repo for paper on TPM key certification verification

  TeX

  •0•0•0•0•Updated Aug 4, 2023Aug 4, 2023

• cvm-client

  Public
  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

  •0•0•0•0•Updated Jun 2, 2023Jun 2, 2023