On integrating confidentiality and functionality in a formal method

DOI10.1007/S00165-013-0285-4MaRDI QIDQ736833zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Unifying theories of confidentiality
• scientific article; zbMATH DE number 1746450
• Informational analysis of security and integrity
• Non-interference through determinism
• Abstractions preserving parameter confidentiality

Cites work

• scientific article; zbMATH DE number 3943003 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 1122463 (Why is no real title available?)
• scientific article; zbMATH DE number 2080001 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• scientific article; zbMATH DE number 1884405 (Why is no real title available?)
• A UTP semantics for \textsf{Circus}
• A refinement strategy for Circus
• Communication Theory of Secrecy Systems*
• Compositional noninterference from first principles
• Integrated Formal Methods
• Preservation of probabilistic information flow under refinement
• Protocols for authentification and key establishment
• The B-Book
• The Miracle of Reactive Programming
• The shadow knows: refinement and security in sequential programs
• Unwinding Possibilistic Security Properties

Cited in

(3)

• CoCon: a conference management system with formally verified document confidentiality
• A stepwise approach to linking theories
• Unifying theories of confidentiality

Describes a project that uses

Uses Software

• Z
• Circus

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q736833)