Tool support for Confidentiality by Construction
In many software applications, it is necessary to preserve confidentiality of information. Therefore, security mechanisms are needed to enforce that secret information does not leak to unauthorized users. However, most language-based techniques to enable information flow control work post-hoc, deciding whether a specific program violates a confidentiality policy. In contrast, we have proposed a refinement-based approach to derive programs that preserve confidentiality-by-construction in previous work. This approach follows the principles of Dijkstra’s correctness-by-construction. In this extended abstract, we present the implementation and tool support of that refinement-based approach allowing to specify the information flow policies first and to create programs which comply to these policies by construction. In particular, we present the idea of confidentiality-by-construction using an example and discuss the IDE we have developed.
Mon 5 NovDisplayed time zone: Guadalajara, Mexico City, Monterrey change
13:30 - 15:00 | |||
13:30 45mTalk | Tool support for Confidentiality by Construction HILT S: Tobias Runge TU Braunschweig, S: Ina Schaefer Technische Universität Braunschweig, Alexander Knüppel TU Braunschweig, Germany, Loek Cleophas Eindhoven University of Technology (TU/e) and Stellenbosch University, Derrick Kourie Stellenbosch University, Bruce Watson Stellenbosch University; and Centre for AI Research, CSIR | ||
14:15 45mOther | Panel on Language-based Security HILT P: Stephen Chong Harvard University, Ina Schaefer Technische Universität Braunschweig, Tobias Runge TU Braunschweig, Lucas Wagner Rockwell Collins, Sam Procter Carnegie Mellon Software Engineering Institute, Tucker Taft AdaCore |