Miracles happen and are now formalized. Moreover, they can exist in formal methods where functionality and confidentiality of systems coexist in efforts to build secure systems by design. Functionality and confidentially have so far been irreconcilable attributes in formal systems.

In Banks and Jacob’s paper, inconsistencies between confidentiality and functionality are referred to as miracles. The formal techniques they present aim at “verifying that a system design’s functionality and confidentiality attributes are mutually consistent, and for ensuring that consistency is maintained by refinement steps.”

The formal method is based on the Circus formalism and can be easily extended to any formal methods within this family. While functionality in formal methods is of predominant concern, confidentiality is emphasized here. The paper shows how confidentiality can be highlighted and coexist with functionality, and be verifiable. Circus is elevated to accommodate for the inferences of adversarial users.

What do we get at the end? We get an approach where refinement steps do not compromise the feasibility of a process design. Now software can be developed to be secure without deep knowledge of security. While no tool exists yet to support this approach, the moment when it is available may not be far off.

The paper is written with ultimate rigor, ample details, and examples. The formalisms are explained and easy to follow. It is self-contained, and anyone with some background in formal system can start immersing him/herself easily into a world where miracles happen--and when they do, they are contained.