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 Systems35 (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 ... )
Verification (D.4.6 ... )
Security and Protection (D.4.6 )
Specifying And Verifying And Reasoning About Programs (F.3.1 )
Would you recommend this review?
Other reviews under "Semantics": Date
The semantics of programming languages: an elementary introduction using structural operational semantics
Hennessy M., John Wiley & Sons, Inc., New York, NY, 1990. Type: Book (9780471927723)
Jul 1 1991
Logic of domains
Zhang G., Birkhäuser Boston Inc., Cambridge, MA, 1991. Type: Book (9780817635701)
Mar 1 1993
A linear-history semantics for languages for distributed programming
Francez N., Lehmann D., Pnueli A. Theoretical Computer Science 32(1-2): 25-46, 1984. Type: Article
Jul 1 1985

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy