Hauptinhalt

DFG-SPP RS3 (2010-2012)

Project Description

The objective of this project is to develop an approach for considering advanced techniques in access control (in particular delegation of user permissions) in the context of a formally-based software development methodology. The approach will be based on formalizations from the Secure Information Flow approach to security verification, which offers the possibility for a particularly fine-grained security analysis. Since secure information flow formalizations have traditionally been used in the context of mandatory access control (MAC) which does not usually include user-level permission delegation, investigation of delegation in this context has so far been limited. Since the Secure Information Flow approach has found increasing use over the last few years, one of the goals of this project is therefore to fill this gap by investigating how to support the analysis of sophisticated access control techniques such as delegation of user permissions. A further objective is to exploit results on modular analysis of Secure Information Flow properties in the context of the analysis of access control mechanisms and in particular the delegation of user permissions. The scientific progress to be made will be transferred into the context of a secure software development approach based on formal verification tool support. They will be validated using an application from the e-health sector (in collaboration with existing projects in this domain at Fraunhofer ISST, where the Principal Investigator of this project holds a secondary position). Main results of the project will include the following:

• A theory supporting the modular analysis of user permission delegation in the context of secure information flow models.
• Integration into the context of a secure software development approach based on formal verification tool support.
• Automated tools for formal verification based on SMT solvers (such as Z3).
• Validation through an application in an e-health system including access control with delegation.

Publications

• Jan Jürjens, Loïc Marchal, Martín Ochoa, Holger Schmidt: Incremental Security Verification for Evolving UMLsec models in Robert B. France, Jochen Malte, Behzad Bordbar, Richard F. Paige(editors) : Springer Lecture Notes in Computer Science pp.52-68 Modelling Foundations and Applications - 7th European Conference, ECMFA 2011, Birmingham, UK, June 6 - 9, 2011 Proceedings. 2011
  

  @INPROCEEDINGS{DBLP:conf/ecmdafa/JurjensMOS11,
  author = {Jan J{\"u}rjens and Lo\"ic Marchal and Mart\'in Ochoa and Holger
  Schmidt},
  title = {Incremental Security Verification for Evolving UMLsec models},
  booktitle = {Modelling Foundations and Applications - 7th European Conference,
  ECMFA 2011, Birmingham, UK, June 6 - 9, 2011 Proceedings},
  year = {2011},
  editor = {Robert B. France and Jochen Malte K{\"u}ster and Behzad Bordbar and
  Richard F. Paige},
  volume = {6698},
  series = {Lecture Notes in Computer Science},
  pages = {52-68},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/ecmdafa/2011},
  doi = {http://dx.doi.org/10.1007/978-3-642-21470-7_5},
  isbn = {978-3-642-21469-1}
  }

  
  [Show BibTex]  [DOI]  

• Frank Hadasch, Andreas Lehmann, Stefan Pfeiffer, Thomas Ruhroth, Thomas Stocker: RS3 Reference Scenario: Enterprise Systems (Static Analysis). 2012
  

  @MISC{berichtES,
  author = {Frank Hadasch and Andreas Lehmann and Stefan Pfeiffer and Thomas
  Ruhroth and Thomas Stocker},
  title = {{RS3 Reference Scenario: Enterprise Systems} (Static Analysis)},
  year = {2012}
  }

  
  [Show BibTex]  

• M. Ochoa, J. Jürjens , D. Warzecha: A Sound Decision Procedure for the Compositionality of Secrecy in Springer pp.97--105 4th International Symposium on Engineering Secure Software and Systems (ESSoS'12). 2012
  

  @INPROCEEDINGS{DBLP:conf/essos/OchoaJW12,
  author = {M.~Ochoa and J.~J{\"u}rjens and D.~Warzecha},
  title = {A Sound Decision Procedure for the Compositionality of Secrecy},
  booktitle = {4th International Symposium on Engineering Secure Software and Systems
  (ESSoS'12)},
  year = {2012},
  volume = {7159},
  series = lncs,
  pages = {97--105},
  publisher = {Springer},
  ee = {http://dx.doi.org/10.1007/978-3-642-28166-2_10}
  }

  
  [Show BibTex]  

• B. Köpf , L. Mauborgne, M. Ochoa: Automatic Quantification of Cache Side-Channels in Computer Aided Verification (CAV 2012). 2012
  

  @INPROCEEDINGS{KMO12,
  author = {B.~K\"{o}pf and L.~Mauborgne and M.~Ochoa},
  title = {Automatic Quantification of Cache Side-Channels},
  booktitle = {Computer Aided Verification (CAV 2012)},
  year = {2012},
  series = lncs,
  publisher = sv,
  note = {Accepted for publication}
  }

  
  [Show BibTex]  

• M. Ochoa: TU Dortmund. 2012 To be submitted (PhD-Thesis)
  

  @PHDTHESIS{Och12,
  author = {M.~Ochoa},
  school = {TU Dortmund},
  year = {2012},
  note = {To be submitted}
  }

  
  [Show BibTex]  

• M. Ochoa, J. Jürjens, J. Cuéllar : Non-interference on UML State-charts in Springer LNCS pp.15pp. 50th International Conference on Objects, Models, Components, Patterns (TOOLS Europe 2012). 2012
  

  @INPROCEEDINGS{OchoaJCTools12,
  author = {M.~Ochoa and J.~J\"urjens and J.~Cu\'{e}llar},
  title = {Non-interference on {UML} {S}tate-charts},
  booktitle = {50th International Conference on Objects, Models, Components, Patterns
  (TOOLS Europe 2012)},
  year = {2012},
  series = {LNCS},
  pages = {15pp.},
  publisher = {Springer},
  note = {To appear}
  }

  
  [Show BibTex]  

• New Entry: UNPUBLISHED: Modeling secure information flow properties with {UMLsec} and their Analysis using {MAKS}Thomas Ruhroth, Jan J\"urjens,