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

Integration of a Security Type System into a Program Logic

Reiner Hähnle (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)) ; Jing Pan ; Philipp Rümmer ; Dennis Walter
Theoretical Computer Science (selected papers from TGC 2006) (0304-3975). Vol. 402 (2008), 2-3, p. 172-189.
[Artikel, refereegranskad vetenskaplig]

Type systems and program logics are often thought to be at opposing ends of the spectrum of formal software analyses. In this paper we show that a flow-sensitive type system ensuring non-interference in a simple while-language can be expressed through specialised rules of a program logic. In our framework, the structure of non-interference proofs resembles the corresponding derivations in a state-of-the-art security type system, meaning that the algorithmic version of the type system can be used as a proof procedure for the logic. We argue that this is important for obtaining uniform proof certificates in a proof-carrying code framework. We discuss in which cases the interleaving of approximative and precise reasoning allows us to deal with delimited information release. Finally, we present ideas on how our results can be extended to encompass features of realistic programming languages such as Java.

Nyckelord: Language-based security, Information-flow analysis, Dynamic logic, Security type system, Formal verification

Denna post skapades 2009-01-05.
CPL Pubid: 83504


Läs direkt!

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

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)
Institutionen för data- och informationsteknik, datavetenskap (GU) (GU)


Datavetenskap (datalogi)

Chalmers infrastruktur