Tutorial

[senier]

• Preconditions

  • [ ] GNAT Studio: RecordFlux syntax
  • [ ] GNAT Studio: RecordFlux menu entry (check, generate)
  • [ ] RecordFlux: format
  • [ ] GNAT Studio: Location view integration

• Tutorial

  • [ ] Create simple spec (ICMP?)
    • Fields
    • Conditions
    • Enumeration
    • Refinements (?)
  • [ ] Demonstrate (detection of) specification errors
    • exclusive conditions
    • contradiction
    • reachability
  • [ ] Create prototype in Python
  • [ ] Generate SPARK code
  • [ ] Implement SPARK driver
  • [ ] Proof SPARK program
    • Demonstrate proof error due to invalid usage
    • Gold level
  • [ ] Compile and run program
    • Ping host
    • Notice issue in spec
  • [ ] Demonstrate matching sample against sample (dissector PoC)
    • Adapt spec
    • Regenerate, re-proof, re-run
  • [ ] Outlook
    • Fuzzer
    • FSM

[senier]

Done in #370