CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A Per Model of Secure Information Flow in Sequential Programs

Andrei Sabelfeld (Institutionen för datavetenskap ; Institutionen för datavetenskap, ProSec) ; David Sands (Institutionen för datavetenskap ; Institutionen för datavetenskap, ProSec)
Higher-Order and Symbolic Computation Vol. 14 (2001), 1, p. 59-91.
[Artikel, refereegranskad vetenskaplig]

This paper proposes an extensional semantics-based formal specification of secure information-flow properties in sequential programs based on representing degrees of security by partial equivalence relations (pers). The specification clarifies and unifies a number of specific correctness arguments in the literature, and connections to other forms of program analysis. The approach is inspired by (and equivalent to) the use of partial equivalence relations in specifying binding-time analysis, and is thus able to specify security properties of higher-order functions and partially confidential data. We extend the approach to handle nondeterminism by using powerdomain semantics and show how probabilistic security properties can be formalised by using probabilistic powerdomain semantics.



Denna post skapades 2006-09-28. Senast ändrad 2017-09-14.
CPL Pubid: 18077

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för datavetenskap (1993-2001)
Institutionen för datavetenskap, ProSec (2002-2004)

Ämnesområden

Datavetenskap (datalogi)

Chalmers infrastruktur