transparent gif


Ej inloggad.

Göteborgs universitets publikationer

Integration of a Security Type System into a Program Logic

Författare och institution:
Reiner Hähnle (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers), Chalmers); Jing Pan (-); Philipp Rümmer (Institutionen för data- och informationsteknik, datavetenskap (GU)); Dennis Walter (-)
Utgiven i serie vid Göteborgs universitet:
Technical report - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University, ISSN 1652-926x; nr 2007:1
Antal sidor:
Sammanfattning (abstract):
Type systems and program logics are often conceived 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 recent 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 like Java.
Ämne (baseras på Högskoleverkets indelning av forskningsämnen):
Data- och informationsvetenskap ->
Datavetenskap (datalogi)
program logics, program verification, secure information flow, type systems
Postens nummer:
Posten skapad:
2007-04-17 19:01
Posten ändrad:
2013-08-13 14:32

Visa i Endnote-format

Göteborgs universitet • Tel. 031-786 0000
© Göteborgs universitet 2007