Hopefully, the contents of this paper will convince key players of the cryptocurrency community to assess the application of formal methods more thoroughly.


Subtleties and Traps with Security Properties
Security properties have proved to be unexpectedly complex to grasp and formalize. One of the fundamental reasons for this is that security properties are not safety properties (w.r.t. the Alper-Schneider framework [1]}). Most of the verification methods, results and tools developed for almost half a century by the Software Engineering community have been aimed at safety properties. Then, most of them fall short when dealing with security properties. Only very recently some of these methods and tools have been adapted for the problem of security properties.
For instance, safety properties enjoy, what is some times called, the refinement property. This means that, if \(S\)  is the description of a system verifying safety property \(F\)  and \(S^{\prime }\)  is a more deterministic refinement of \(S\) , then \(S^{\prime }\)  (automatically) verifies \(F\) . However, in general, security properties do not enjoy the refinement property. This means that even if you have proved that \(S\)  verifies security property \(F\)  and that \(S^{\prime }\)  is a refinement of \(S\) , then you cannot assert that \(S^{\prime }\)  verifies \(F\) . The problem is that there are implementation decisions that in spite of generating a more deterministic system, they might introduce security issues. A typical example is the specification of the values stored in the memory cells delivered by the operating system to a process. At a certain level of abstraction these values might be underspecified which implies that, potentially, any value can be stored. Assume you can prove that this is secure. Afterwards, programmers decide to deliver the cells with the values left by the last process that used that buffer. Although this is an implementation of the first specification it is blatantly insecure.
On the other hand, reasoning about implementations provides the ultimate guarantee that
deployed mechanisms behave as expected. However, due to the issues mentioned above, formally proving non-trivial security properties of code might be an overwhelming task in terms
of the effort required, especially compared w.r.t. proving functional correctness (i.e. a safety property). In addition,
many implementation details are orthogonal to the security properties
to be established. This implies that slight changes in the implementation technology might have devastating consequences as concerns the security of the implementation. Therefore, complementary approaches are needed when non-trivial security properties are at stake:

Verification is performed on idealized models that abstract away the specifics of any particular implementation, and yet provide a realistic setting in which to explore the security issues that pertain to the realm of those (critical) mechanisms.

Additionally, verification is performed on more concrete models where low level mechanisms (such as pointer arithmetic) are specified.

Finally, the low level model is proved to be a correct implementation of the idealized model.

A particular class of the idealized models mentioned above are those called security models. These models have played an important role in the design and evaluation of high assurance security systems. Their importance was already pointed out in the Anderson report [2]}. The
paradigmatic Bell-LaPadula model [3]}, conceived in 1973, constituted the first big effort on providing a formal setting in which to study and reason on confidentiality properties of data in time-sharing mainframe systems.
