TU Darmstadt / ULB / TUbiblio

An Automatic Inference of Minimal Security Types

Bollmann, Dominik and Lortz, Steffen and Mantel, Heiko and Starostin, Artem :
An Automatic Inference of Minimal Security Types.
Proceedings of the 11th International Conference on Information Systems Security (ICISS)
[Conference or Workshop Item] , (2015)

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.

Item Type: Conference or Workshop Item
Erschienen: 2015
Creators: Bollmann, Dominik and Lortz, Steffen and Mantel, Heiko and Starostin, Artem
Title: An Automatic Inference of Minimal Security Types
Language: English
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.

Title of Book: Proceedings of the 11th International Conference on Information Systems Security (ICISS)
Uncontrolled Keywords: Engineering; E3
Divisions: Department of Computer Science
Department of Computer Science > Modeling and Analysis of Information Systems (MAIS)
DFG-Collaborative Research Centres (incl. Transregio)
DFG-Collaborative Research Centres (incl. Transregio) > Collaborative Research Centres
Profile Areas
Profile Areas > Cybersecurity (CYSEC)
DFG-Collaborative Research Centres (incl. Transregio) > Collaborative Research Centres > CRC 1119: CROSSING – Cryptography-Based Security Solutions: Enabling Trust in New and Next Generation Computing Environments
Date Deposited: 06 Sep 2018 11:03
Export:

Optionen (nur für Redakteure)

View Item View Item