Partial notes to How to Write Formally Verifiable Specifications in Python The talk slides Problem: Mutable objects Due to aliasing, writing to a reference may implicitly modify values obtained via other references. In the F/V context, it invalidates what we know about affected memory locations. Tracking aliasing and re-establishing properties can significantly complicate reasoning. Solution Use immutable objects (non-destructive updates). Can be facilitated by pyrsistent library.

We (TxRx team, ConsenSys) have implemented a Fork Choice compliance test generator as well as have generated Fork Choice compliance test suites. Overall F/C compliance testing methodology is described here. In this report we briefly describe the results of the initial implementation phase (i.e. the F/C test generator and F/C test suites). A more detailed description of the work is TBD. This work was supported by a grant from the Ethereum Foundation. Implementation status Test generator

Fork Choice compliance testing Implemented test generator (initial phase). Test suites are generated: tiny (135 tests), small (1472 tests) and standard (13240 tests). Next steps: performance improvements test generator improvements coverage-guided fuzz testing

Our ultimate goal is to ensure that FC implementations conform to the FC spec. The ultimate way to reach the goal would be employing formal verification of the FC implementations, however, we assume that it's beyond our reach at present time. Therefore, testing is the only practical approach to reach our goal. It's still very challenging though and in the write-up we analyze how the problem can be solved efficiently. The methodology is implemented in the fc-compliance branch of eth2.0-specs fork. To be merged into the main repo. Preliminary research has been done in this repo. Summary of proposed ideas Here is the summary of the proposed ideas, which will be described in more details later. employ "multiplicative" coverage criterion, which takes into account interactions of FC spec and FC implementation behavior. In particular,obtain coverage with two step approach: 1) obtain a good coverage of the FC spec, and then, 2) fuzz the above test suite to improve FC implementation coverage according to the "multiplicative" criterion. Both blind and client-specific coverage-guided fuzzing can be used.

A Python to Dafny transpiler intended to process Ethereum-related specifications. Project Abstract The Ethereum-related specifications (like consensus specs, execution specs, DV specs) are not defined formally, while their core parts are expressed in Python. As a consequence, one cannot reason about such specs directly and has to express them in some verification-friendly language. This translation likely results in bugs introduced, which questions whether one can really trust the conclusions of such approach. We believe that the most practical way to overcome the problem is to a) define the translation mechanically, and b) thoroughly test it. To reduce testing and implementation efforts, we: a) chose Dafny as the target language (as Dafny supports imperative and impure code), b) designed a simple and concise direct imperative impure transpiler, c) supporting a subset of Python. NB Additionally, there already is a number of Etherem-related F/V projects using Dafny, e.g. Eth2.0 spec in Dafny, F/V of DVT protocol, EVM interpreter in Dafny. *[F/V]: Formal Verification *[DV]: Distributed Validator

Abstract Beacon chain protocol critically depends on clock synchronization. If validators or nodes clocks discrepancy becomes too much, then liveness properties can become violated, i.e. the protocol participants won't be able to make progress or its probability becomes too low. In theory, safety properties can become violated too, since validators which failed to participate due to clock discrepancies are penalized. If an adversary manages to attack otherwise honest validator clocks then it can seize voting power over time. Safety, liveness and robustness Casper FFG is based on epoch justification and finalization. An epoch justification requires 2/3 of total voting power, so if an adversary gains control on 2/3 then it will reign over a Casper FFG based system. If an adversary controls less than 2/3 of voting power, but it controls 1/3, it might be able to hinder protocol progress, by voting differently than other validators, thus breaking liveness property. However, even if an adversary controls less than 1/3 of voting power, there are other sources of failures in real network. E.g. there are network delays, clock disparities, hardware or link failures. All these result in additional faults, which combined with an adversarial behavior of some nodes can lead to situations when epochs cannot get justified for some periods of time. So, from a practical point of view, while protocol can successfully withstand safety and liveness attacks, it can do that with degrade performance, which is a real problem for real users of the protocol. While, in theoretical sense, liveness property cannot be violated in a finite execution of a protocol, a practical liveness as perceived by real users can be violated.

In the write up, we are discussing theoretical foundations of Onotole - a transpiler for a subset of Python used for beacon chain specs development. It turned to be an effective tool in practice: several problems in the py-specs have been found and it's been used to regularly translate the py-spec to an implementation in Kotlin, which is the base for a Phase1 simulator developed by @mkalinin, which is, in its turn, is used in Eth1-Eth2 merger research. Before extending the Onotole to support translations to other languages, we want to formulate (and clarify) the principles, it's based on, which can be useful in a more general context, for formal engineering of blockchain protocols. The Onotole tool is a (simple) example of four principles we will discuss: it's a tool, built using meta-programming approach for a Python subset used for the beacon chain specs development (tailoring formal methods to a problem domain) which is used to translate the py-specs (formal spec engineering) to a statically typed language so that a light(er)-weight formal method (static type checking) can be employed

Onotole is an experimental transpiler, whis is intended to translate Ethereum Proof-of-Stake Consensus Specifications, expressed in a (statically-typed) subset of Python to other languages, like Kotlin, Java, Dafny, etc. NB I am using "beacon chain specs" also to refer to the Ethereum Proof-of-Stake Consensus Specifications, for historical reasons. In a wider/longer perspective, the goal is to attach formal semantics to the subset of Python, so that there is a solid formal foundation for the Eth PoS Consensus specifications. Basically, it tries to alleviate the fact that Python doesn't have a formal specification and there is lack of formal method tools (though, there exist some, like MyPy or Nagini). This is a short overview, there is a longer (but largely outdated) description: part 1, part 2 and part 3. Transformation phases python parsing

In the context of formal reasoning about imperative programs, one often faces frame problem. However, literature, addressing the problem that we have read, lacks simple and concise intuition of how the problem is solved. In particular, while comparing two papers, Dynamic Frames and Separation Logic, it becomes clear the papers use varying terminology. While their approaches look rather similar, it was not evident how their actually can be compared. We address the problems by developing a simple unified model, which solves the framing problem (in the context of formal reasoning about imperative programs). We intend to use the model to compare approaches of Dynamic Frames and of Separation Logic. Hopefully, it will also serve as a relatively simple description of how the frame problem can be tackled. The write-up is also a follow up to Why pure functional form matters, which discusses an approach to avoid "dangerous" aliasing (less expressive obviously). Frame problem We are starting from the following understanding of the frame problem (from Frame problem's wiki page):

Short term Time in Ethereum2.0 Time requirements Clock Synchronization Protocol NTP attacks, implications, countermeasures Hybrid security models

In the write-up, we are comparing how Separation Logic (abbreviated as SL) and Dynamic Frames Theory (abbreviated as DFT) tackle the frame problem. This turned to be a non-trivial, but quite useful exercise, at least, for me. One problem is that the DFT is not explicit about some of its foundations, so we need to recover details. Another problem is that terminology differs and variable, state, value and address refer to somewhat different notions. Third, underlying logics used to express framing specification are different too. So, we first clarify the problem, unify terminology and then discuss differences and similarities in tackling the frame problem. Frame problem and (absence of) aliasing The approaches of DFT and SL to tackle the frame problem are quite similar: one adds necessary annotations (framing specifications) and use them to prove absence of aliasing. However, terminology and details differ significantly. In order to unify approaches, we have developed a simple model of how absence of aliasing can be proved. We will use the model (its terminology and proof principle) to compare the DFT and the SL.

Beacon chain specification developers chose Python as the language to express executable parts of the Eth2 beacon chain spec (referenced to as pyspec hereinafter). One of the most important benefit here is that a Python code is easy to read and write for general audience. Even if a programmer is not familiar with Python (but is familiar with some other popular programming language), it's not difficult to read the spec - and to learn necessary features. The pyspec developers facilitate this further by limiting themselves to a subset of Python features: a statically typed subset, avoiding of tricky Object-Oriented features, etc. However, in the formal method context, there is an obvious downside: Python support from formal method tools is almost absent. Two notable exceptions are mypy and Nagini, both are built upon statically typed Python subset (PEP-484). Lack of tool support additionally complicates formal work, which is already quite (or even extremely) complicated. At the same time, blockchain application require very high level of software quality, as bugs can be costly and difficult to fix after deployment. Which makes employment of formal methods inevitable. There can be several ways to overcome the problem. One is to (regularly) translate the pyspec and its updates to a language that is more suitable for formal work (e.g. beacon chain in Dafny, beacon chain in K Framework). Even more ambitious would be to develop the executable parts of the spec in a language with better formal grounds. Both approaches have downsides: synchronizing developments in two languages is costly and error-prone, while a better language from a formal point of view will be more difficult to comprehend for a general audience. Tailored semantics & tools We explore another approach: enrich the pyspec with (formal) semantics of the Python subset employed. This facilitates implementing a mechanical translation of the pyspec to other languages, including those with the state-of-the-art support from formal method tools. At the same type, the pyspec can be developed in (a subset of) Python.

(Py)Spec Formal Engineering slides: https://hackmd.io/@ericsson49/pyspec-formal-engineering My background S/W engineer, mostly Financial S/W Familiar with Formal Methods for a long time Mostly around Coq and SMT/SAT solvers didn't have a (good) chance to apply as S/W Engineer

The Clock Sync approach, we have discussed, can be viewed as an example of Decentralized Trustless Oracle (DTO). Reference clocks (for a common time standard) can be seen both as sensors or as oracles. In the clock sync approach, the reference clocks are attached to nodes, forming a distributed network of sensors/oracles. Individual sensors/oracles may fail, so a robust aggregation method is applied to fuse multiple sensors/oracles and obtain an accurate time estimates. The aggregation process can be replicated on every node, resulting in a decentralized oracle, which need not be trusted to the extent that the robust aggregation method is able to tolerate faults. There are several topics inspired by the analogy between sensors and oracles that we'd like to explore: clock sync approach analysis from DTO perspective how the clock sync/sensor fusion paradigm can be extended to construct DTOs in general role of time for oracles The write up concentrates on the first one. The rest are to be discussed in following write ups.

Lighter-weight formal methods A widely used idea to simplify introduction of formal methods is start from lighter formal methods, which suffer from less soundness or precision, but are more practical, i.e. requiring less annotation burden and/or less theorem proving. There is a wide spectrum of such methods, starting from static type checking to a full-blown verification. Actually, even when considering verification only, there can variations, depending on the amount of code base to be trusted, which can differ tremendously among approaches to verify software (e.g. see here some other link??). Annotation burden One way to describe a formal method 'weightiness' is the complexity of annotation, required to assist formal reasoner: simple methods can work with simple (often already existing) annotations, while full-blown verification requires not only extensive code annotations (like pre-/post-conditions, assertions, invariants, etc), but writing auxiliary lemmas and developing proof search procedures. The annotation burden can be a serious obstacle, especially during early development stages, where codebase can be quite unstable (it can help finding problems earlier too, though we assume this to be a separate activity, loosely coupled with the main s/w development process, e.g. like prototyping). lightweight formal methods: static type checking middleweight formal methods: Extended Static checking, (bounded) Model Checking

This is a follow up post to Formal Engineering for Blockchains, which discusses the beacon chain protocol specifics. Intro There is a growing interest to applying formal methods in industrial software engineering. It's perhaps mostly apparent in areas, where software quality is critical, which is exactly the case for the blockchain protocol implementations. Consequences of bugs in such software can be quite costly or even devastating. Even if a bug is not severe, deploying a fix in a distributed BFT setup can be a problem, if such a fix affects consensus. By their nature, blockchains are designed to be resilient to arbitrary faults and thus a bug fix can be seen as a form of a byzantine fault. For the reason, blockchain software evolution and maintenance would be easier, if bugs were wiped out. While it's impossible in general, formal methods can wipe out certain classes of bugs. In the write up, we want to discuss how the benefits can be brought to the beacon chain protocol development, however the ideas can be applicable to other blockchains as well. Our emphasis is on the engineering side: what are the problems, possible solutions and what can be done to improve the situation. The emphasis also means that we mostly concentrate on coding/engineering aspects, i.e. on bugs and problems arising during protocol specification and implementation. Though higher level analysis of the protocol definitely can (and does) benefit from application of formal methods, we mostly ignore this aspect here. One (minor) reason is that such work is already conducted by other teams. More importantly, a high-level analysis often assumes simplified versions of protocols. However, industrial-strength specifications and implementations necessarily add lots of low-level details. And software engineers need tools and approaches to manage the increased complexity. We thus believe that high-level analysis of protocols and industrial strength implementation are two ends, opposite in some sense and thus require separate treatment. However, it would be definitely great to trace high-level properties down to low-level bits, in some (hopefully not too distant) future.

We have discussed already that time setup vulnerabilities pose a threat to overall beacon chain protocol security properties (eth2.0-specs issue #1592, Time attacks and security models). However, the attacks are perhaps not very realistic, if implemented directly, since the problems will be detected by administrators and necessary counter-measures will be taken. But such attacks can aid more sophisticated and/or stealth attacks. One direction of such opportunistic behavior can be de-anonymization. As an attacker can adjust clocks of vulnerable nodes, it can affect their behavior which is noticeable within some period - i.e. if such a node is validating, then it should attest blocks each epoch and there will be late or early attestations, depending on how the attacker has shifted the clock. It also affects other validator duties like block proposal and attestation aggregation. However, attestation are to be issued each epoch, so it's easier to start from analyzing attestations. A validator becomes proposer very rare, so it's probably not very useful from de-anonymization perspective. De-anonymization attack and setup We assume there is a node or set of nodes, some of them are participants of beacon chain protocol (though extensions to other protocols are possible), i.e. validating nodes, others being non-validating nodes. An attacker cannot control nodes directly, however it can control clocks of some nodes. Each node contains zero or several validators. Each validator possesses a distinct private/public key pair, which means its behavior can be distinguished from other nodes, by monitoring its activity. E.g. someone (not necessarily an attacker) can send a block to the nodes. Then some nodes will attest it according to the beacon chain protocol. As signing keys are different, nodes responses will differ too. During an epoch, all correctly functioning validator nodes should participate (become attesters). Therefore, monitoring node activity allows to determine which validators are associated with the node.

Clock synchronization problem can be seen as a model estimation problem. E.g. one can model a relation between local clock $C_t$ which is to be synchronized with a reference clock $R_t$ as $R_t = offset + C_t + e_t$, where $offset$ is clock difference to be estimated and $e_t$ absorbs left-over errors. Alternatively, one can pose the clock synchronization as a prediction of reference clock readings, based on an available time source. After the model is estimated (i.e. value of the $offset$), based on sample readings, one can approximating the reference time, using the available clock (clocks) and the model $E(R_t) = offset + C_t$. In a robust estimation setting, when (a significant portion of) $e_t$ may be arbitrarily large, one can use median or other robust method, to estimate the $offset$. When $C_t$ and/or $R_t$ are interval data, one can use Marzullo's algorithm or Brooks-Iyengar algorithm to obtain an interval estimate of the $offset$. The model above is extremely simple, basically, it has no (estimated factors, though prediction depends on a local clock, which rate is fixed and assumed to be known (for simplicity, we assume the rate is 1, if it is different but known, one can adjust $C_t$ definition appropriately). One can re-arrange terms to make it more evident $R_t-C_t = offset + e_t$. In practice, more complex models are often required, as clocks are drifting, i.e. clock rate varies over time, but the variation can be predicted or explained by other factors, leading to more complex models.

This is a follow up of Sensor Fusion for BFT Clock Sync, Time as a Public Service in Byzantine context and Time attacks and security models writings. The goal of the write up is to design protocol architecture to address clock sync problems in BFT context. Clock sync protocols can be rather simple, but it can be hard to reach precision and accuracy guarantees when arbitrary faults are possible and there are lots of participating nodes. There are three factors, which can help to solve the problem in practice: a) reference clocks, synchronized to a common Time Standard, b) independent local clocks and c) uncertainty of clock drift and network delays. Requirements Protocol requirements There are two group of requirements to the protocol: precision and accuracy bounds, i.e. time estimates of participants should be close to each other (precision) and close to the common time standard (accuracy)

This is a follow up post to Verifiable Precompiled Contracts to address issues that have been identified during a discussion with Casey Detrio and Alex Beregszaszi. Modern cryptography like Elliptic Curve and ZKP is highly desired to be run inside blockchain transactions. However, this is a hard target. Blockchain client implementers are conservative about new bits of codes and this behavior is highly justified: software bugs are ubiquitous and bugs can result in direct losses or render system unusable (e.g. in-determinism can break consensus). Careful audit is required, which is labor-intensive. The problem is amplified when compiled execution is required, which is the case since performance is critical for ZKP and many other cryptography algorithms. To solve the problem, one may employ formal verification, which can guarantee absence of some classes of bugs, though it is labor-intensive too. Another consequence is that introduces new code to trust. This is a difficult task, which lies on intersection of verification and compilation technologies, both of them being far from trivial. In the post, we discuss opportunities to optimize overall efforts to sandbox compiled execution in the domain of cryptography primitives. In many cases, codes in the domain may be relatively easy to analyze, since restricted languages and formal models can be enough. The analysis of such languages and models can be orders of magnitude easier and often allows implementation of push-button approach to verification. Overview