Bollmann, Dominik ; Lortz, Steffen ; Mantel, Heiko ; Starostin, Artem (2015)
An Automatic Inference of Minimal Security Types.
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (Abstract)
Type-based information-flow analyses provide strong end-to-end confidentiality guarantees for programs. Yet, such analyses are not easy to use in practice, as they require all information containers in a program to be annotated with security types, which is a tedious and error-prone task - if done manually. In this article, we propose a new algorithm for inferring such security types automatically. We implement our algorithm as an Eclipse plug-in, which enables software engineers to use it for verifying confidentiality requirements in their programs. We experimentally show our implementation to be effective and efficient. We also analyze theoretical properties of our security-type inference algorithm. In particular, we prove it to be sound, complete, minimal, and of linear time-complexity in the size of the program analyzed.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2015 |
| Autor(en): | Bollmann, Dominik ; Lortz, Steffen ; Mantel, Heiko ; Starostin, Artem |
| Art des Eintrags: | Bibliographie |
| Titel: | An Automatic Inference of Minimal Security Types |
| Sprache: | Englisch |
| Publikationsjahr: | 2015 |
| Buchtitel: | Proceedings of the 11th International Conference on Information Systems Security (ICISS) |
| Kurzbeschreibung (Abstract): | Type-based information-flow analyses provide strong end-to-end confidentiality guarantees for programs. Yet, such analyses are not easy to use in practice, as they require all information containers in a program to be annotated with security types, which is a tedious and error-prone task - if done manually. In this article, we propose a new algorithm for inferring such security types automatically. We implement our algorithm as an Eclipse plug-in, which enables software engineers to use it for verifying confidentiality requirements in their programs. We experimentally show our implementation to be effective and efficient. We also analyze theoretical properties of our security-type inference algorithm. In particular, we prove it to be sound, complete, minimal, and of linear time-complexity in the size of the program analyzed. |
| Freie Schlagworte: | Engineering; E3 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Modellierung und Analyse von Informationssystemen (MAIS) DFG-Sonderforschungsbereiche (inkl. Transregio) DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche Profilbereiche Profilbereiche > Cybersicherheit (CYSEC) DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche > SFB 1119: CROSSING – Kryptographiebasierte Sicherheitslösungen als Grundlage für Vertrauen in heutigen und zukünftigen IT-Systemen |
| Hinterlegungsdatum: | 06 Sep 2018 11:03 |
| Letzte Änderung: | 18 Apr 2019 13:23 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum