The shadow knows: refinement and security in sequential programs

DOI10.1016/j.scico.2007.09.003zbMath1178.68166OpenAlexW2019193016MaRDI QIDQ923889

Carroll Morgan

Publication date: 24 July 2009

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2007.09.003

zbMATH Keywords

securityprivacyimplementationspecificationHoare logiclogic of knowledge

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Theory of software (68N99)

Related Items (12)

Program Synthesis Using Dual Interpretation ⋮ Dynamic intransitive noninterference revisited ⋮ Architectural refinement and notions of intransitive noninterference ⋮ Security invariants in discrete transition systems ⋮ Compositional refinement in agent-based security protocols ⋮ Compositional noninterference from first principles ⋮ How to Brew-up a Refinement Ordering ⋮ Hidden-Markov program algebra with iteration ⋮ Algebraic foundations for quantitative information flow ⋮ Abstractions of non-interference security: probabilistic versus possibilistic ⋮ On integrating confidentiality and functionality in a formal method ⋮ Preface

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The dining cryptographers problem: Unconditional sender and recipient untraceability
• Power domains
• A semantic approach to secure information flow
• A Proof System for Information Flow Security
• Knowledge and common knowledge in a distributed environment
• The Shadow Knows: Refinement of Ignorance in Sequential Programs
• Abstraction, Refinement and Proof for Probabilistic Systems
• An axiomatic basis for computer programming
• Program development by stepwise refinement
• A per model of secure information flow in sequential programs

This page was built for publication: The shadow knows: refinement and security in sequential programs