article

Verified Safety and Information Flow of a Block Device

Author:

Paul GraunkeAuthors Info & Claims

Electronic Notes in Theoretical Computer Science (ENTCS), Volume 217

Pages 187 - 202

https://doi.org/10.1016/j.entcs.2008.06.049

Published: 01 July 2008 Publication History

Abstract

This work reports on the author's experience designing, implementing, and formally verifying a low-level piece of system software. The timing model and the adaptation of an existing information flow policy to a monadic framework are reasonably novel. Interactive compilation through equational rewriting worked well in practice. Finally, the project uncovered some potential areas for improving interactive theorem provers.

References

[1]

Chen, C.-P. and P. Hudak, Rolling your own MADT - a connection between linear types and monads, in: ACM Symposium on Principles of Programming Languages, 1997, pp. 54--66

Crossref

Google Scholar

[2]

Claessen, K. and J. Hughes, Quickcheck: a lightweight tool for random testing of Haskell programs, in: ACM SIGPLAN International Conference on Functional Programming, New York, NY, USA, 2000, pp. 268--279

Digital Library

Google Scholar

[3]

Denning, D.E., A lattice model of secure information flow. Communications of the ACM. v19. 236-243.

Crossref

Google Scholar

[4]

Felleisen, M., “The Calculi of #v-CS Conversion: A Syntactic Theory of Control and State in Imperative HigherOrder Programming Languages,” Ph.D. thesis, Indiana University (1987)

Crossref

Google Scholar

[5]

Fox, A.C.J., Formal specification and verification of ARM6, in: International Conference on Theorem Proving in Higher Order Logics (2003), pp. 25--40

Crossref

Google Scholar

[6]

Goguen, J.A. and J. Meseguer, Security policies and security models, in: IEEE Symposium on Security and Privacy, 1982, pp. 11--20

Crossref

Google Scholar

[7]

Gordon, M.J.C., HOL: A machine oriented formulation of higher order logic, Technical Report 68, University of Cambridge Computer Laboratory (1985)

Google Scholar

[8]

Greve, D., M. Wilding and W.M. Vanfleet, A separation kernel formal security policy, in: Fourth International Workshop on the ACL2 Theorem Prover and Its Applications, 2003

Google Scholar

[9]

Haftmann, F. and T. Nipkow, A code generator framework for Isabelle/HOL, Technical Report 364/07, Department of Computer Science, University of Kaiserslautern (2007)

Google Scholar

[10]

Principles of Program Design. 1975. Academic Press.

Crossref

Google Scholar

[11]

Paulson, L.C., Isabelle: The next 700 theorem provers, Logic and Computer Science (1990), pp. 361--386

Google Scholar

[12]

Strachey, C. and C.P. Wadsworth, Continuations: A mathematical semantics for handling full jumps, technical monograph PRG-11, Technical report, Oxford University Computing Laboratory, Programming Research Group (1974)

Google Scholar

[13]

von Oheimb, D., Information flow control revisited: Noninfluence = Noninterference + Nonleakage. In: Samarati, P., Ryan, P., Gollmann, D., Molva, R. (Eds.), LNCS, 3193. pp. 225-243.

Google Scholar

[14]

Wadler, P., The essence of functional programming, in: ACM Symposium on Principles of Programming Languages, 1992, http://homepages.inf.ed.ac.uk/wadler/topics/monads.html

Digital Library

Google Scholar

Cited By

View all

Nelson LBornholt JKrishnamurthy ATorlak EWang X(2020)Noninterference specifications for secure systemsACM SIGOPS Operating Systems Review10.1145/3421473.342147854:1(31-39)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421478
Van Der Meyden RZhang C(2013)Information flow in systems with schedulers, Part IITheoretical Computer Science10.1016/j.tcs.2013.01.002484(70-92)Online publication date: 1-May-2013
https://dl.acm.org/doi/10.1016/j.tcs.2013.01.002

Recommendations

Modal Hyperdoctrine: Higher-Order and Non-normal Extensions
Logic, Language, Information, and Computation
Abstract
Lawvere hyperdoctrines give categorical semantics for intuitionistic predicate logic but are flexible enough to be applied to other logics and extended to higher-order systems. We return to Ghilardi’s hyperdoctrine semantics for first-order modal ...
Extensional Higher-Order Paramodulation in Leo-III
Abstract
Leo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with ...
Theorem Proving Modulo
Abstract
Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Electronic Notes in Theoretical Computer Science (ENTCS)

Electronic Notes in Theoretical Computer Science (ENTCS) Volume 217, Issue

July, 2008

228 pages

ISSN:1571-0661

Issue’s Table of Contents

Publisher

Elsevier Science Publishers B. V.

Netherlands

Publication History

Published: 01 July 2008

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Nelson LBornholt JKrishnamurthy ATorlak EWang X(2020)Noninterference specifications for secure systemsACM SIGOPS Operating Systems Review10.1145/3421473.342147854:1(31-39)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421478
Van Der Meyden RZhang C(2013)Information flow in systems with schedulers, Part IITheoretical Computer Science10.1016/j.tcs.2013.01.002484(70-92)Online publication date: 1-May-2013
https://dl.acm.org/doi/10.1016/j.tcs.2013.01.002

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Modal Hyperdoctrine: Higher-Order and Non-normal Extensions

Extensional Higher-Order Paramodulation in Leo-III

Theorem Proving Modulo