Sciweavers

TCS
2008

Integration of a security type system into a program logic

13 years 11 months ago
Integration of a security type system into a program logic
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. As an additional benefit we obtain uniform certificates for verified programs. We discuss in what 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.
Reiner Hähnle, Jing Pan, Philipp Rümmer,
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TCS
Authors Reiner Hähnle, Jing Pan, Philipp Rümmer, Dennis Walter
Comments (0)