Lattice-Based Information Flow Control-by-Construction for Security-by-Design
| Autor: | Alexander Knüppel, Ina Schaefer, Tobias Runge, Thomas Thüm |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Soundness
050101 languages & linguistics Correctness CORC Computer science Programming language 05 social sciences 02 engineering and technology Construct (python library) USable computer.software_genre Secure by design 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Confidentiality Information flow (information theory) computer computer.programming_language |
| Zdroj: | Proceedings of the 8th International Conference on Formal Methods in Software Engineering. |
| Popis: | Many software applications contain confidential information, which has to be prevented from leaking through unauthorized access. To enforce confidentiality, there are language-based security mechanisms that rely on information flow control. Typically, these mechanisms work post-hoc by checking whether confidential data is accessed unauthorizedly after the complete program is written. The disadvantage is that incomplete programs cannot be interpreted properly and information flow properties cannot be built in constructively. In this work, we present a methodology to construct programs incrementally using refinement rules to follow a lattice-based information flow policy. In every refinement step, confidentiality and functional correctness of the program is guaranteed, such that insecure programs are prohibited by construction. Our contribution is fourfold. We formalize refinement rules for the constructive information flow control methodology, prove soundness of the refinement rules, show that our approach is at least as expressive as standard language-based mechanisms for information flow, and implement it in a graphical editor called CorC. Our methodology is also usable for integrity properties, which are dual to confidentiality. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|