Static Analysis

The focal point of the project is the development of analyses that, on the one hand, provide useful information for the security and safety of systems and, on the other hand, are able to deal with large programs that are subsequently modified. A number of promising approaches exist for developing suitable analyses with varying degrees of precision and cost e.g. Type and Effect Systems and Flow Logics . Aspects of analysis techniques which are important are modularity and expressiblility of control flow analysis.

Documents


  • Hanne Riis Nielson and Flemming Nielson. Flow Logic: a multi-paradigmatic approach to static analysis. SECSAFE-DAIMI-001.
  • Flemming Nielson and Hanne Riis Nielson. Flow Logic for Imperative Objects. SECSAFE-DAIMI-002.
  • Rene Rydhof Hansen. Flow Logic for Carmel. June 28, 2002. SECSAFE-IMM-001. ( .pdf)
  • Rene Rydhof Hansen. Extending the Flow Logic for Carmel. June 28, 2002. SECSAFE-IMM-003.
  • Marc Eluard and Thomas Jensen. Constraint-based security analysis for the Java Card firewall. SECSAFE-IRISA-002. ( .ps)
  • Thomas Jensen and Fausto Spoto. Class Analysis of Object-Oriented Programs through Abstract Interpretation. SECSAFE-IRISA-005.
  • David Clark, Chris Hankin, and Sebastian Hunt. Information Flow for Algol-like Languages . SECSAFE-ICSTM-002. ( .ps)
  • Alessandra Di Pierro, Herbert Wiklicky and Chris Hankin. Approximate Non-Interference . SECSAFE-ICSTM-007. ( .pdf)
  • Mikael Buchholtz, Hanne Riis Nielson and Flemming Nielson. Experiments with Succint Solvers . February 12, 2002. SECSAFE-IMM-002. ( .pdf)
  • Rene Rydhof Hansen. Implementing the Flow Logic for Carmel. November 13, 2002. SECSAFE-IMM-004. ( .pdf)
  • Hongyan Sun, Hanne Riis Nielson and Flemming Nielson. Data Structures in the Succint Solver . November 11, 2002. SECSAFE-IMM-005. ( .pdf)
  • Rene Rydhof Hansen. A Prototype Tool for JavaCard Firewall Analysis. November 13, 2002. SECSAFE-IMM-006. ( .pdf)
  • Frederic Besson, Thomas de Grenier de Latour and Thomas Jensen. Secure Calling Contexts for Stack Inspection . November 15, 2002. SECSAFE-IRISA-006. ( .pdf)
  • C. Bodei, M. Buchholtz, P. Degano, F. Nielson and H. Riis Nielson. Automatic Validation of Protocol Narration . August 12, 2003. SECSAFE-IMM-007. Internal.
  • Flemming Nielson, Hanne Riis Nielson and Hongyan Sun. Observation Predicates in Flow Logic September 3, 2003. SECSAFE-IMM-010. Internal.