Data 61 Meeting Notes November 2019

Misc Notes (Day 1?)

• MBSE- Model-Based Software Engineering

• Technical Areas

  • TA1: Cyber Requirements
  • TA2: Tool development(Us)
  • TA3: ?
  • TA4: Usability, Scalabilitiy
  • TA5: Integration
  • TA6: Platform Providers- Demo platform (Experimental=UXAS, Real=Rotocraft, Raython=Missle Platform)
  • TA7: Evaluators

• Vagrant- VM Management tool

• Monitor component- multiple input signals, collect traces of inputs for analysis.

• Designing SeL4 componentized systems:

  • Transforming existing system with added isoloation properties (VMs)
  • New native seL4 components

• One CASE objective: Re-engineer existing monolithic system to conform to AADL infrastructure

  • Some manual transforms, some can be automated.

• Baseline platform (no cyber protections/isolation): AADL model is only descriptive.

• Ground station on demo platform: kept abstract, functionality "faked" with an instance of the UXAS SendMessage service.

  • Message groups:
    1. Internal to aircraft
    2. Map data
    3. Attestation Requests

Attack on Attestation

• Supply chain attacks are out of scope

  • i.e. we know the golden Ground Station is acceptable

• Ground Station is corrupted after boot

  • OR spoofed version (with access to private keys)

Attestation on Ground Station

• RESOLUTE clause to verify AM lives on GS and is booted into a valid state

• AADL Model that doesn't connect to anything (leaves a dangling port for comm to the ground station)

• TODO: what is Resolint tool?

• Distinguish between AM message well-formedness and an AM Appraisal check pass/fail.

Monitor Types (AADL)

• Syntactic vs Semantic

  • Syntactic: All messages are well formed
  • Semantic(behavioral): Every response is preceded by a request.

• Past-time LTL: Extension of LTL (Linear Temporal Logic) that is provably equal to LTL without past-time primitives.

  • Arguably more expressive for expressing properties of system traces in the past.
  • Time has a beginning => DFA representable
    • i.e. we can generate a verified CakeML filter to check the property.

• Interesting approach: An "Accepting state" causes an alert.

  • Accepting state here is a bad state, a violation of the property.

• Example LTL for above behavioral property: H (resp -> Z(~resp S req))

• TODO: Would a monitor be useful to model interacting with multiple ground stations?

Assurance Case Meeting

• Goal: System meets all of its cyber-resilliancy requirements

  1. Verification of components (individually)
  2. Validation that design meets cyber requirements

• To consider:

  • Formalization step
  • System flow property

• Verify glue-code pattern once, re-use at interface to components

• HAMMER tool (TODO: look at Hammer(K-state?))

  • Config params in Hammer can re-target to seL4, Linux, etc.
  • No new dataflows
  • Maping from AADL to software component topology
  • Alloy (TODO: look at Alloy) step: graph representation of info flow at model level + caMKeS flows.
    • Proves a graph isomorphism between two levels

CakeML/Camkes Breakout Session

• Walked through producer/consumer example in camkes repo
• Cakeml -> basis -> Marshalling prog script
• CompilerScript- onlyprinttypes
• Cake -types < prog.cml
• Textioprogscript
• Double backtick = concrete syntax cakeml

Chat with Kent Mcleod (Data 61 kernel engineer)

• He has some good ideas of how we might measure components in seL4.

The gist of it is that we would add a new connector type to camkes (other connectors are RPC, shared memory, etc.). That connector would be called something like “monitor” and it would use capDL to give one component (restricted) access to the data and code regions of another component. I think it’s a neat solution. Allows us to stay within Camkes and get all the isolation properties we need. But also gives more flexibility to measure an entire component (and make it read only rather than read/write as it would be with shared memory). Would also be cool to make a contribution to cakmes.

CakeML concrete syntax (rather than embedded in HOL)

Thomas (at Collins) has also been tinkering with this. Expressed concern (like Grant had) that new versions of cakeml compiler keep breaking this functionality. I was disappointed (but not altogether surprised) to find out from Johannes that this is not a priorty at data61 at the moment. Johannes' attitude was effectively: "just use HOL". On a brighter note, Kent Mcleod (kernel engineer) expressed an interest in support for cakeml concrete syntax. Seemed to say there is a small contingent of such folks at data61. Although he is not involved directly with the proofs. He will try to rally support at data61 and is willing to stay in touch and help with problems we have in this area.