AnaStaSec

(publicly available)

presentation summary objectives and scientific challenges scientific program meetings and affiliated events participants publications

(restricted access)

deliverables meeting materials

AnaStaSec: Deliverables

  1. Task 0: Coordination
    1. Submitted proposal
    2. Intermediary scientific report (T18)
    3. Slides for the midterm evaluation (T18)
    4. Intermediary scientific report (T30)
    5. Final scientific report (T48)
  2. Task 1: Protocol analysis
    1. D1.1: Analysis of the ARINC823 public key protocol
      2. report - analysis results
    2. D1.2: Analysis of the ICAO9880-IV protocols
      3. deliverable
    3. D1.3: Analysis of the ICAO9896 protocols
      4. deliverable
    4. D1.4: Updated version of ProVerif
      5. read me - ProVerif - documentation
    5. D1.5: Updated version of CryptoVerif
      6. read me - CryptoVerif
  3. Task 2: Security properties
    1. D2.1: Properties of a platform monitor
    2. D2.2: Properties of binary applications
    3. D2.3: Properties of C applications
    4. D2.4: Properties of protocol implementations
      5. source code - report (Sect. 1-2-3)
  4. Task 3:
    1. D3.1: Analysis of a core of the host platform with AstréS
    2. D3.2: Code annotations to be used in Frama-C
    3. D3.4: Analysis of a significiant subset of the host platform and trusted applictions with AstréS
      4. Analysis of the host platform and case studies - Analysis of SBGE
    4. D3.5: Analysis of protocol implementation
      5. report (Sect. 3-4)
    5. D3.6: Synthesis of the use of static analysis for proving security properties in avionic source code
  5. Task 4: Binary code analysis and isolation
    1. D4.1: CompCert for Software Fault Isolation
    2. D4.2: Design and methodology for analysis of security properties linked with dynamic memory allocation
    3. D4.3: Binary validator of SFI properties
    4. D4.4: SFI toolchain</LI>
    5. D4.5: Prototype for analysis of security properties linked with dynamic memory allocation
  6. Task 5:
    1. D5.1: Methodology for integrating AnaStaSec static analysis results in CSPN evaluation scheme
    2. D5.2: Methodology for integrating AnaStaSec static analysis results in Common Criteria scheme
    3. D5.3: Draft proposal for integrating AnaStaSec static analysis results in the ED-203 norm