Hauptinhalt

DFG-SPP RS3 (2010-2012)

Projektbeschreibung

Das Ziel dieses Projektes ist die Berücksichtigung moderner Berechtigungssteuerung in Verbindung mit formalen Softwareentwicklungsmethoden. Der Ansatz basiert auf den Formalisierungen des Secure-Information-Flows zur Sicherheitsverifikation. Dieser bietet die Möglichkeit für besonders detaillierte Sicherheitsanalysen. Da diese Formalisierungen traditioneller Weise im Kontext von Mandatory-Access-Control (MAC) benutzt werden und diese üblicherweise keine Vergabe von Rechten auf Benutzerebene beinhalten, war die Entwicklung in diesem Kontext bislang begrenzt. Da der Secure-Information-Flow-Ansatz in den letzten Jahren immer öfter zum Einsatz kommt, ist eins der Ziele dieses Projektes diese Lücke zu füllen. Im Rahmen des Projektes wird untersucht, wie die Analyse von komplexen Zugriffsteuerungstechniken, wie der Delegation von Berechtigungen unterstützt werden kann. Ein weiteres Ziel ist es, die Ergebnisse der modularen Analyse der Secure-Information-Flow-Eigenschaften im Zusammenhang der Zugriffssteuerungsmechanismen und der Delegation der Berechtigungen zu nutzen. Die wissenschaftlichen Ergebnisse werden dann in den Rahmen der Entwicklung sicherer Software basierend auf formaler Verifikation übertragen. Durch eine konkrete Anwendung im E-Health-Bereich werden diese Entwicklungen überprüft. Diese Anwendung findet in Zusammenarbeit mit bereits bestehenden Projekten des Fraunhofer ISST statt. Die wichtigsten Ergebnisse werden sein:

• Eine Theorie zur Unterstützung der modularen Analyse der Delegation von Berechtigungen in Secure-Information-Flow-Modellen
• Die Integration in den Ansatz zur Entwicklung sicherer Software basierend auf formaler Verifikation
• Automatisierte Werkzeuge für eine formale Verifikation basierend auf SMT (wie Z3)
• Validierung durch Anwendung in einen E-Health-System mit Delegation der Berechtigungen

Publikationen

• 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,