Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Dependent type theory for verification of information flow and access control policies
Nanevski A., Banerjee A., Garg D.  ACM Transactions on Programming Languages and Systems 35 (2): 1-41, 2013. Type: Article
Date Reviewed: Sep 5 2013

Security issues are a growing concern in an increasingly connected society. Given the central role played by programming languages in the implementation of information technology systems, introducing such matters early in the specification phase of programs could have a significant impact on their reliability.

To address this problem, the authors introduce relational Hoare type theory (RHTT), a typing framework that combines dependent typing (types may depend on values) with a logic for asserting confidentiality policies in programs. Using languages equipped with this formalism, programmers may specify and check that their programs satisfy sophisticated information flow properties such as authentication, authorization, or declassification. Within RHTT, data is labeled as either high (confidential) or low (public), with the goal of ensuring that programs do not leak any sensitive information. RHTT assertions are relational predicates in which the behaviors of two arbitrary runs of a program can be related, paving the way to the specification of the program’s noninterference property: a low output must not depend on high inputs, thus preventing information leakage. The logic part of RHTT makes reasoning about such properties possible. The overall system has been formally specified, and the authors have machine-checked its soundness, using the Coq theorem prover.

While this abstract, theoretical paper addresses an important issue, the audience is likely limited to researchers well versed in type theory and automated proof assistants. However, even though the material is dense, the authors have done a good job of presenting it in a pedagogical manner.

Reviewer:  P. Jouvelot Review #: CR141516 (1311-1016)
Bookmark and Share
Semantics (D.3.1 ... )
Pre- And Post-Conditions (F.3.1 ... )
Security and Protection (D.4.6 )
Specifying And Verifying And Reasoning About Programs (F.3.1 )
Verification (D.4.6 ... )
Would you recommend this review?
Other reviews under "Semantics": Date
 FOO: a minimal modern OO calculus
Gerakios P., Fourtounis G., Smaragdakis Y.  FTfJP 2015 (Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, Prague, Czech Republic,  Jul 7, 2015) 1-4, 2015. Type: Proceedings
Oct 7 2015
ECMA-335 static formal semantics
Vasenin V., Krivchikov M.  Programming and Computing Software 38(4): 183-188, 2012. Type: Article
Jan 24 2013
Towards a categorical foundation for generic programming
Hinze R., Wu N.  WGP 2011 (Proceedings of the 7th ACM SIGPLAN Workshop on Generic Programming, Tokyo, Japan,  Sep 18, 2011) 47-58, 2011. Type: Proceedings
Mar 29 2012

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2017 ThinkLoud, Inc.
Terms of Use
| Privacy Policy