[FEATURE] TA2 properties of interest

[podhrmic]

Summary

Properties of interest for OpenSUT, ordered by priority (highest first):

1. classical correctness properties (the absence of Undefined Behavior - leading to memory safety and a lack of runtime errors) - currently mandated in this requirement
   • signed integer over and underflow
   • use of an uninitialized variable
   • oversized shift amount
   • out of bounds array access
   • null pointer dereferencing
   • NOTE: absence of UB does not guarantee memory safety, as programmer's error can still lead to memory leaks (although it is much harder to make a mistake that way)
   • Ensure allocation of SHA256 context in sha_256.c
   • covers PROVERS properties from Appendix A: Memory safety, Undefined behavior, Structural data properties
2. Functional correctness properties - builds on top of UB. Specify which FC properties
   • linear arithmetic constraints - e.g. string processing in OpenSUT
   • loop invariants - zero initialize an array and code in actuation_logic.c
   • simple ownership properties - secure boot attest()
   • multidimensional array access that is out of order - actuation_collect_trips()
   • user defined spec functions - actuate_actuator() or merge sort from the CN tutorial
   • Lynx pseudocode - can this be turned into a CN spec? Galois only link
   • covers PROVERS properties from Appendix A: Functional Correctness
3. abstract/finite state machines as described in [FEATURE] CN for encoding abstract state machines (ASMs) #114
   • an-airport-simulation example in the CN-tutorial
   • FSMs are derived from the requirements/system model, ASMs might be too general for CN (can be handled in model checkers first, such as SAL)
   • covers PROVERS properties from Appendix A: State Machine Adherence, API Usage Patterns
4. information flow analysis
   • a notion of Security levels - we have low and high data, and low is not influenced by high (can be generalized to multiple levels of security)
   • re-use the approach taken by JML
   • covers PROVERS properties from Appendix A: Data-flow restrictions
   • TL;DR; A security level is a set of heap locations. A declassification is part of the method contract.
     • Chapter 13 from the Deductive SW verification book
     • The Key Project
       • includes a symbolic debugger Eclipse plugin (video)
       • using the symbolic debugger for a proof inspection (video)
     • Deductive Verification of Information Flow Properties of Java Programs (lecture)
   • an alternate approach is SPARK/Ada - annotate which variable the output depends on [blog post]
5. separation
   • driven by CAST-32A
   • emphasis on WCET and Robust Resource/Time Partitioning as well as Critical configuration of the Multi Core Processor
   • Robust Resource/Time Partitioning
     • basically a proof of Time/Space separation provided by the OS/Hypervisor:
     • Resource Partitioning requirements

       • Software partitions cannot contaminate the storage areas for the code, I/O or data of other partitions.

       • Software partitions cannot consume more than their allocations of shared resources.

       • Failures of hardware unique to a software partition cannot cause adverse effects on other software partitions.

     • Time Partitioning Requirements

       • is achieved when, as a result of mitigating the time interference between partitions hosted on different cores, no software partition consumes more than its allocation of execution time on the core(s) on which it executes, irrespective of whether partitions are executing on none of the other active cores or on all of the other active cores.

     • in the absence of a proof, can generated tests suffice?
     • even seL4 might fall short here, as it is making idealistic assumptions about the HW
     • unclear how to validate the HW itself
   • Information Flow Analysis is necessary, but a full separation proof is clearly out of scope for CN
   • Resource analysis can be done statically with AADL CAMET tools, for the dynamic resource allocation and behavior, we would like to know if the flow management/queue management algorithms behave correctly even when resources are exhausted (e.g. a queue is full, a free buffer is not available) - see the LynxOS network buffer example

Acceptance Criteria

• Take these priorities into consideration, and develop a plan to implement an example.
• Tie each property to real-world motivation, highlighting why it is important for the system
• Tie to requirements document in OpenSUT
• Provide examples for each category

References

(check the box once he reference was reviewed)

UB resources

• A guide to UB: https://blog.regehr.org/archives/213
• What everyone should know about UB: https://blog.llvm.org/2011/05/what-every-c-programmer-should-know.html

Memory safety resources

• TRACTOR announcement: https://www.darpa.mil/news-events/2024-07-31a
  • links to CISA The Case for Memory Safe Roadmaps: https://www.cisa.gov/case-memory-safe-roadmaps
    • which links to various other sources about memory safety
      • including CWEs and other references
  • links as well to The White House directive: https://www.whitehouse.gov/oncd/briefing-room/2024/02/26/memory-safety-fact-sheet/
• Other resouces:
  • CSET: https://cset.georgetown.edu/article/memory-safety-an-explainer/

Other resources

• Cerberus homepage: https://www.cl.cam.ac.uk/~pes20/cerberus/
• Eliminating Memory Safety Vulnerabilities at the Source
  • memory safe languages for new code

[bcpierce00]

I want to hear more about (3) -- am surprised that hyperproperties could be provable with CN just as it stands...

…

Message ID: ***@***.***>

[podhrmic]

Info about information flow properties from @kiniry :

The line of work ends with researchers at KSU and KIT (separately). See, e.g., Beckert et al. 2014, Schmitt and Ulbrich 2015, and Amtoft et al. 2010.

A lot of it starts with Warnier's PhD thesis in 2006 and my group's work in the 00s.

There are additional papers from Robby, David Naumann, Janota+Grigore+Moskal in '07 (my PhD students), case studies using KeY from Grahl and Scheben in the KeY Book and from Do et al. (most of which are based on my group's work on formal methods for electronic voting), and more.

[podhrmic]

I want to hear more about (3) -- am surprised that hyperproperties could be provable with CN just as it stands...

@bcpierce00 the Ariport simulation example in the CN tutorial captures what I had in mind - I am imagining that lot of the specs in that example can be auto generated from a system model

[bcpierce00]

Are there any hyperproperties in the airport example??

[podhrmic]

The example is a simple FSM, no hyperproperties. I think that is sufficient for our use case, and the scope of the project - does that sound reasonable to you? I should clarify this in the issue description.

[bcpierce00]

OK, that's clearer. I wish we had a real example, though, to replace the Airport one -- that one is a bit made up and it's actually a bit confusing when you get into the details.

[podhrmic]

@thatplguy have a look at 4 and 5!