Haskell Attestation Manager

Overview

---

The Haskell Attestation Manager is a collection of Haskell libraries and executables that support the design and prototyping of layered attestation protocols. It builds off of the Copland effort to provide a concrete implementation of the Copland semantics and a testing ground for experimental extensions (to both the Copland language proper and its supporting envioronment).

We have ongoing work to implement similar Attestation Managers in other language environments(see: Copland Software), and our JSON message exchange format is designed to facilitate communication amongst protocols whose executions span these diverse environments. The ultimate goal of the Copland effort is to build formally verified attestation protocols and infrastructure. This prototype serves as a testing ground towards that goal.

Please send questions/comments to Adam Petz([email protected]) or submit a GitHub issue.

Installation

---

Dependencies

• Haskell Stack: https://docs.haskellstack.org/en/stable/README/
• Haskell AM source: https://github.com/ku-sldg/haskell-am.git

QuickStart Guide

1. Install Haskell Stack (via instructions at the link above)
2. Clone the haskell-am source repository (git clone https://github.com/ku-sldg/haskell-am.git)
3. In the top-level of that repository: type make
   • NOTE: this may take a while (~20-30 minutes) the first time due to the Haskell dependencies.
4. Type make run
5. Successful installation/execution will include output that ends with something like "Appraise Result:" followed by a pretty-printed evidence value (the result of executing a hard-coded Copland protocol).

Examples

---

make run

make run executes the following command:

cd copland-interp ; stack exec -- ${CLIENT} -a -w -v.

This runs the Appraiser Client with options to spawn all necessary child nodes (CVM and ASP servers) and perform appraisal of the resulting evidence. The Copland term executed by default is the hard-coded value local_term in the main function of the Appraiser Client executable source file (copland-interp/client_app/ClientMain.hs). Alternative example Copland phrases to run (commented out below local_term) are in the source file: copland-interp/src/Example_Phrases_Concrete.hs.

stack exec is the Haskell Stack command for running executables managed by one of its projects. ${CLIENT} is the variable for the Appraiser Client executable in the Makefile, whose name is originally defined in the stack project cabal file(copland-interp/copland-interp.cabal). cd copland-interp is necessary because we must be within the stack project directory(copland-interp/) to run stack exec. See the Haskell Stack documentation for more details on stack exec.

Haskell AM Executables

---

The Haskell AM project is organized as logically distinct executables:

1. Attestation Manager Client (Appraiser Client)
2. Copland Virtual Machine Server (CVM Server)
3. Attestation Service Provider Server (ASP Server)
4. Datatype/JSON Generator and Translator

These executables share common libraries(see Source Files section below). Their purpose and usage are described individually in the following sections.

---

Attestation Manager Client (Appraiser Client)

The Appraiser Client can generate nonces, sequence exection of multiple Copland phrases, gather evidence results, provide evidence results as initial evidence to other Copland phrase executions, and perform appraisal over evidence. It is responsible for sending the first request during an attestation protocol run, and also performs the final appraisal.

• -w (--spawnCvms) spawns CVM servers as separate background threads before performing the client actions. This option is useful for testing purposes- it alleviates the hassle of configuring and starting each server as its own executable. Uses with auto-generated port string addresses: CVM_P (where P is its place ID) for all places involved in the Copland term executed.
• -v (--spawnAsps) Spawn ASP servers (with auto-generated port string addresses: ASP_P_I, where P is its place and I its ASP_ID) as separate background threads for all ASPs at all places involved in the Copland term executed.
• -a (--appraise) Perform appraisal on the resulting evidence.

• The main module for the Appraisal Client is ClientMain.hs
• Type make helpclient for a complete description of Appraiser Client command line options (Only options documented here are currently supported).

---

Copland Virtual Machine Server (CVM Server)

Documentation forthcoming...

---

Attestation Service Provider Server (ASP Server)

Documentation forthcoming...

---

Datatype/JSON Generator and Translator

There are two primary functions of the Generator/Translator:

1. Generate random well-formed Haskell ADTs(Abstract Data Types) and JSON objects relevant to our Attestation Manager
2. Translate to/from ADTs and their JSON representation

It is meant to be useful for testing against implementations outside of the Haskell ecosystem. It can provide well-formed test inputs, and it can also act as an oracle for JSON parsing. The Haskell ADT definitions are here: CoplandLang.hs. A formal description of the ADT grammars and their JSON representations are here: Copland terms and JSON.

• You must provide EXACTLY ONE of the following options: -t(Copland Phrase), -e(Concrete Evidence), -y(Evidence Type), -q(RequestMessage), -p(ResponseMessage), -s(SigRequestMessage), -u(SigResponseMessage), -k(AspRequestMessage), -m(AspResponseMessage), to specify the type of thing you'd like to generate/translate.
• If -d is set, the OUTPUT will be the Haskell ADT representation. Otherwise the OUTPUT will be the JSON representation.
• Generator Mode: -n N will generate N random things of the type you specify and output them newline-separated.
• Translator Mode: If -n N is NOT set (or if N==0), the executable becomes a translator to/from JSON and the ADT representations. The input representation is always opposite of the output representation(determined by -d). For example: if -d is set the input will be JSON and the output will be the ADT (and vice-versa if -d is NOT set).
• If -l is set: use local datatypes specified in Haskell concrete syntax, defined in Main module of generator executable: gen_app/GenMain.hs, functions with names that start with "local_vals_".
• -i FILENAME optional input file (stdIn if omitted)
• -o FILENAME optional output file (stdOut if omitted)
• NOTE: input and output terms/JSON are always newline-separated.
• The main module for the Generator and Translator is GenMain.hs
• Type make helpgen for a complete description of the Generator/Translator command line options.

Advanced Configuration

---

Some advanced configuration will be necessary during development (while working within the stack project). To persist environment variables upon exiting a terminal session, consider adding the export commands to your shell startup configuration (i.e. .profile for MacOS).

Environment Variables

• COPLAND_BUILD : Point to top level of the haskell-am repository (parent directory of stack project).
  • export COPLAND_BUILD=<haskell-am_repo>
  • Used internally for configuration (i.e. to find the default key file if COPLAND_KEY is not defined).
• COPLAND_KEY: specifies a custom key file for signing.
  • export COPLAND_KEY=<path_to_key>
  • This will take priority over the COPLAND_BUILD environment variable.

Command-Line Options

• See the help text (make help) for complete syntax and quick descriptions of options for all three executables. To see the help text for individual executables: , make helpclient, make helpserver, make helpgen.
• See the Makefile(in this directory) for commented working examples of command line option combinations.

Development Flow/Hints

• The easiest strategy for an interactive development style is via invoking the make ghci* family of commands from the repo toplevel. These invoke the stack ghci feature to load a familar Haskell ghci REPL environment within the stack project (that reacts to source modifications). See the Haskell Stack documentation for more details.
• Because stack ghci only allows loading one Main module at a time, we need separate commands that respond to changes in the source code of each Main module independently: make ghciclient(client_app/ClientMain.hs), make ghciserver(server_app/ServerMain.hs), make ghcigen(gen_app/GenMain.hs).
• make ghci loads code for the main stack project executable (copland-interp), which effectively loads all shared library source files (ignoring the client/server/gen executable sources). If you've changed code in multiple Main modules, a safe bet is to simply type make(an alias for stack build). However, this will not give you a REPL loop and usually takes quite a bit longer(10-20 seconds) than simply re-loading a ghci session (via :r)--so it is best used sparingly (i.e. before deploying everything for an end-to-end test run).
• Useful ghci commands (once in a ghci REPL session):
  • :r -- reload a session (re-runs type checker after source file changes).
  • :q -- quit a ghci session
  • :i <expression> -- print out useful info about a Haskell expression (its type, where it is defined, etc.).
  • :t <expression> -- check the type of a Haskell expression

Source Files

---

All Haskell source files are within the stack project directory (copland-interp/). Within that directory, the Main modules for executables are in the sub-directories: client_app/(ClientMain.hs), server_app/(ServerMain.hs), and gen_app/(GenMain.hs). The source files extracted from the formal specification are in the sub-directory: extracted_src/. The rest of the common library source files are under the sub-directory: src/ .

Main Module source files

---

• client_app/ClientMain.hs: Main module for Appraiser Client.
  • Top-level Attestation Manager/Appraiser: Configures and initiates Copland protocol evaluations and orchestrates appraisal of result evidence.
  • Command-line args defined in src/ClientProgArgs.hs
• server_app/ServerMain.hs: Main module for Attestation Server.
  • Standalone Attestation Server: Handles requests to interpret Copland phrases within a Copland Virtual Machine (CVM) execution environment.
  • Command-line args defined in src/ServerProgArgs.hs
• gen_app/GenMain.hs: Main module for Generator/Translator.
  • Generates random well-formed attestation datatypes (Copland terms and Evidence) and their corresponding JSON objects. Also can be configured for bi-directional translation between the datatypes and their JSON representation.
  • Command-line args defined in src/GenProgArgs.hs

Extracted code from Coq

---

• extracted_src/*: Haskell source files core to execution of attestation and appraisal, extracted directly from a formal specification in Coq.
  • For descriptions of these source files, see the README of the Coq spec here: https://github.com/ku-sldg/copland-avm.
  • To preserve formal properties, these files should not be modified after extraction.

Library source files

---

• Appraisal_IO_Stubs.hs: Concrete definitions of primitive appraisal checker functions. Instantiations of (abstract) stubs of the same name in the Coq specification.
• Axioms_Io.hs: Dummy definition of the cvm_events uninterpreted function of the Coq spec. Weird artifact of code extraction that may be refactored away in the future (since unecessary for concrete execution).
• BS.hs: Concrete instantiation of the raw evidence datatype BS (treated abstractly in Coq spec), along with some common BS values and utilities.
• ClientProgArgs.hs: Specifies command-line options for the Appraiser Client main module (client_app/ClientMain.hs).
  • Uses: http://hackage.haskell.org/package/optparse-applicative
• CommTypes.hs: Datatypes relevant to communication (request, response, address representation, server congiguration, etc.).
• CommUtil.hs: Utility library for general communication primitives.
• Copland.hs: Interface module that (for convenience) packages and exports a collection of modules containing datatypes and typeclass instances relevant to Copland language primitives.
• Copland_Concrete.hs: Convenient "concrete syntax" (in Haskell) for Copland phrases.
  • CoplandTerm datatype.
  • Useful for writing Copland phrases by hand during prototyping: top-level primitive constructors (i.e. ASP, SIG, HSH), infix notations for compound terms (i.e. :->:).
  • Includes a translation function (toExtractedTerm :: CoplandTerm -> Term_Defs.Term) to the Coq-extracted Copland syntax used by the AM internally for Copland execution.
• Copland_Display.hs: Pretty-printing for protocol terms and evidence.
  • Uses: http://hackage.haskell.org/package/prettyprinter-1.2.1
• Copland_Gen.hs: Helper functions for generaitng random samples of Copland terms, evidence, and other datatypes; output to a file or stdout.
• Copland_Json.hs: ToJSON/FromJSON instances for Copland language and other attestation-relevant datatypes.
  • Implements data exchange format from here: Copland terms and JSON.
  • Implemented via Haskell's Aeson library for JSON parsing.
• Copland_Qc.hs: (QuickCheck Copland). Helper library to GenCopland.
  • Uses Haskell's QuickCheck library to define Arbitrary instances for terms and concrete evidence.
• CryptoImpl.hs: primitive crypto operations
  • Crypto libraries chosen initially for simplicity, not necessarily for security.
• Cvm_Impl_Wrapper.hs: Convenience wrappers around extracted functions in: extracted_src/Cvm_Impl.hs. Necessary (for now) due to how monads are instantiated/executed at the top level.
• Cvm_St_Deriving.hs: Adds "deriving" clauses to CVM datatypes extracted from the Coq spec (i.e. Show to support printing them in Haskell).
• DemoStates.hs: A collection of configuration parameters/helper functions used to initialize demonstration attestation scenarios.
• Example_Phrases_Admits.hs: Instantiating abstract parameters of Copland phrases extracted from Coq (extracted phrases in file: extracted_src/Example_Phrases.hs).
• Example_Phrases_Concrete.hs
  • Example Copland phrases in concrete syntax (Copland_Concrete.CoplandTerm datatype).
• GenProgArgs.hs: Specifies command-line options for the Generator/Translator executable.
  • Uses: http://hackage.haskell.org/package/optparse-applicative
• IO_Stubs.hs: Concrete instantiations of abstract IO primitives whose stubs are defined in the Coq spec (measurements, crypto, communication).
• MonadAM.hs: Definition of the AM Monad.
  • AM (Attestation Manager) Monad is a computational context for managing attestation protocols.
  • Provides primitives for generating nonces, running multiple Copland phrases, collecting results, and performing appraisal.
  • State Monad Transformer with Reader and IO.
• MonadAM_Types.hs: The AM Monad definition with its state and environment structures, plus execution interfaces.
• MonadCop.hs: Definition of the COP Monad.
  • COP Monad provides a read-only configuration for interpreting Copland phrases during Copland VM (CVM) execution.
  • Reader Monad Transformer with IO.
• OptMonad_Coq.hs: Instantiations of the AM and Opt monads from the Coq spec. For compatibility reasons, both become a state monad transformer in Haskell (for now).
• ServerHandlers.hs: Handler functions for different kind of servers involved in attestation (ASP server, crypto server, CVM server, etc.).
• ServerOpts.hs: Helper functions for constructing server configuration parameters (optionally derived from Copland phrase parameters).
• ServerProgArgs.hs: Specifies command-line options for the Attestation Server executable.
  • Uses: http://hackage.haskell.org/package/optparse-applicative
• ServerUtil.hs: Utility functions to configure and launch servers relevant to attestation.
• StMonad_Coq.hs: Instantiation of the St monad from the Coq spec. Uses a state monad transformer with an underlying Reader + IO (for static environment/attestation config + comm/crypto).
• StringConstants.hs: Constant strings used in pretty-printing and JSON generation.
• Term_Defs_Deriving.hs: Adds "deriving" clauses to Copland language datatypes extracted from the Coq spec (i.e. Show to support printing them in Haskell).
• UDcore.hs: Functions to run UnixDomain Socket clients and servers.