On integrating confidentiality and functionality in a formal method

DOI10.1007/s00165-013-0285-4zbMath1342.68191OpenAlexW2122718698MaRDI QIDQ736833

Michael J. Banks, Jeremy L. Jacob

Publication date: 5 August 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-013-0285-4

zbMATH Keywords

information flow securityCircusconfidentiality propertiesconfidentiality-preserving refinementmiraclesunifying theories of programming

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

A Stepwise Approach to Linking Theories

Uses Software

• Z
• Circus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Compositional noninterference from first principles
• A refinement strategy for Circus
• The shadow knows: refinement and security in sequential programs
• A UTP semantics for \textsf{Circus}
• Protocols for authentification and key establishment
• Preservation of probabilistic information flow under refinement
• The Miracle of Reactive Programming
• Communication Theory of Secrecy Systems*
• The B-Book
• Unwinding Possibilistic Security Properties
• Integrated Formal Methods

This page was built for publication: On integrating confidentiality and functionality in a formal method