Abstract
Non-interference is a security property which states that improper information leakages due to direct and indirect flows have not occurred through executing programs. In this paper we investigate a game semantics based formulation of
non-interference that allows to perform a security analysis of closed and open procedural programs. We show that such formulation is amenable to automated verification techniques. The practicality of this method is illustrated by several examples, which also emphasize its advantage compared to known operational methods for reasoning about open programs.
non-interference that allows to perform a security analysis of closed and open procedural programs. We show that such formulation is amenable to automated verification techniques. The practicality of this method is illustrated by several examples, which also emphasize its advantage compared to known operational methods for reasoning about open programs.
| Original language | English |
|---|---|
| Publication date | 15 Sept 2014 |
| Number of pages | 16 |
| DOIs | |
| Publication status | Published - 15 Sept 2014 |
| Event | International Workshop on Security and Trust Management - University of Wroclaw, Wroclaw, Poland Duration: 10 Sept 2014 → 11 Sept 2014 Conference number: 10 http://stm14.uni.lu/ |
Workshop
| Workshop | International Workshop on Security and Trust Management |
|---|---|
| Number | 10 |
| Location | University of Wroclaw |
| Country/Territory | Poland |
| City | Wroclaw |
| Period | 10/09/2014 → 11/09/2014 |
| Internet address |
Keywords
- Language-based Security
- Algorithmic Game Semantics
- Verification of Non-interference