MeetingNotes - ku-sldg/stairCASE GitHub Wiki

GS Architecture Meeting Notes - 03 May 2019 - 9:30 AM

Participants

  • Adam, Ed, Josiah, Tj, Perry

Agenda

  • Debrief HCSS
  • Discuss Attestation Monad Design

Notes

  • Debriefed HCSS
  • Much discussion of the attestation monad design
    • Fencing Copland terms at runtime. Semantics of Compland remains untouched
    • Variables may appear in terms, but must be instantiated prior to runtime. The executed protocol must fit the Copland standard
    • Variables are defined in the Monad
    • We need an appraisal language that minimally:
      • Checks signatures
      • Decomposes evidence packages (pattern matching maybe)
      • Compares nonces and evidence
      • Holds values (monad binding)
  • Synthesis from evidence description and policy to attestation monad
    • Given [(n||e)]p can we generate a Copland phrase and appraisal function?
    • What intermediate forms are required to get from evidence description to protocol and appraisal function?
    • What policies constrain the protocol?
    • What constraint information is needed to produce a protocol?
    • What elements of the attestation monad will be synthesized vs. treated as boilerplate?

Variable Examples (redux)

I forgot to specify t making the discussion much more complicated than it needed to be. Updated to change that and explicitly specify golden evidence:

do { e <- goldenEv ;
     n <- genNonce ;
     [(e',n’)]p <- @p[n](t);
     if n=n’ and e==e' then return True else Nothing }

where

t = (n | usm) -> SIG
  1. Determine golden evidence and store in e
  2. Generate a nonce and store in n
  3. Evaluate term t at p with initial evidence n
  4. Match generated evidence with [(e,n’)]p
    1. e is bound to evidence
    2. n’ is bound to the returned nonce
    3. [...]p is notation that checks the signature of ... against p and causes the match to fail if sig check failes ::the same trick could be applied to decryption without failure::
    4. return calculates the value of conjuncting nonce and evidence check returning success (Just) or failure (Nothing).

We will assume that base evidence (including nonces) are bit string values.

Actions

  • Lay out tasks for getting to CASE demo
  • Lay out tasks for getting to synthesis
  • Reconcile previous two tasks to eliminate redundancy
  • Write Copland protocols for CASE demo
  • Write Attestation Monad(s) for CASE demo

GS Architecture Meeting Notes - 26 April 2019 - 9:30 AM

Participants

  • Ed, Adam, Tj, Michael, Grant

Agenda

  • Discuss groundstation architecture
  • Discuss adding variables to Copland

Notes

Ground Station

  • Brief the ground station architecture
    • Measurement flow
      • UserAM measures QGroundControl
      • PlatformAM measures Linux kernel running QGroundControl and UserAM
      • seL4AM measures the PlatformAM ::Not necessarily. As a CAmkES component, PlatformAM has strong separation guarantees::
      • seL4AM reports boot evidence from UBOOT
      • UBOOT stores evidence from early boot
    • Attestation flow
      • UAVAM is asked to appraise ground station and checks appraisal cache
        • Cache hit -> terminate with result stored in cache
        • Cache miss -> send attestation request to ground station
      • UAVAM generates a nonce, creates a request, signs request [(n,r]uav
      • UserAM receives attestation request from UAV
        • Validate signature
        • Check QGroundControl attestation cache
          • Cache hit -> terminate with cached evidence
          • Cache miss -> measure QGroundControl and store in cache
        • Check platform attestation cache
          • Cache hit -> terminate with catched evidence
          • Cache miss -> request attestation from PlatformAM
      • UserAM forwards nonce and request to PlatformAM ::unsure of signature necessity here::
      • PlatformAM receives attestation request from UserAM
        • Measure platform (seL4, etc)
        • request attestation from seL4AM
      • seL4AM receives attestation request and returns stored boot evidence and nonce signed
      • PlatformAM receives attestation from seL4AM and returns received evidence, measurement result, and nonce signed
      • UserAM receives attestation from PlatformAM and returns received evidence, measurement result, and nonce signed
      • UAVAM receives attestation from UserAM
        • Checks UserAM signature
        • Checks nonce
        • Checks QGroundControl measurement
        • Checks PlatformAM evidence
          • Checks PlatformAM signature
          • Checks nonce
          • Checks platform measurement
          • Checks seL4AM evidence
            • Cheks seL4AM signature
            • Checks nonce
            • Checks boot measurement
  • Nifty diagram from Tj that captures much of this that I can’t get in any of our documents.
  • What should we prove about our attestation managers?
    • Events happen in the correct order
    • Correct measurements are performed
    • Nonces are not reused or exposed
    • Session keys are not reused or exposed
    • Non-interference

Variables

  • Need for variables in Copland terms
    • Paramterizing terms over place seems quiite sensible for protocol reuse
    • The base Copland term grammar does not include evidence, thus using variables to pass evidence won’t work
    • The base Copland term grammar could support variables whose values are terms allowing reusable libraries
      • Environments of these snippets could be passed using @p(t)
      • Environments would be constants and fully calculuated prior to passing
  • Need for variables in AM terms
    • Holding dynamically created values like nonces and session keys for appraisal
    • Holding results from attestation protocol execution for later appraisal
    • Calculating intermediate appraisal results
    • Pattern matching

Variable Examples

do { n <- genNonce ;
     [(e,n’)]p <- @p[n](t);
     return if n=n’ and (check e) then Just true else Nothing }
  1. Generate a nonce and store in n
  2. Evaluate term t at p with initial evidence n
  3. Match generated evidence with [(e,n’)]p
    1. e is bound to evidence
    2. n’ is bound to the returned nonce
    3. [...]p is notation that checks the signature of ... against p and causes the match to fail if sig check failes ::the same trick could be applied to decryption without failure::
    4. return calculates the value of conjuncting nonce and evidence check returning success (Just) or failure (Nothing).

Much more going on under the hood here of course.

Actions

  • Write attestation protocols for CASE example
  • Define what attestation managers do for CASE example
  • Define places and their properties
  • Define variables and how they are used
  • Define appraisal language ::commands, pattern matching, monad::