# (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 - Joined Eth2 research recently - have a great chance now --- ## My work @TXRX My work @TXRX/PegaSys/ConsenSys: - clock sync, DeFi, oracles - fork choice tests + a bit of bug fixing - pyspec transpilation to Kotlin - pyspec formal engineering But concentrate on the latter here --- ## (Py)Spec ***Formal*** Engineering - Want high quality financial S/W - Bugs can be costly - Even more important for blockchains - Lack of control after deployment ==> Use **Formal** Methods --- ## (Py)Spec Formal ***Engineering*** - Formal Methods are a mostly academic topic - But things are changing - (Very) difficult to employ in a typical industrial setting - ConsenSys, in fact, the first real opportunity for me ==> Concentrate on **Engineering** aspects --- ## ***(Py)Spec*** Formal Engineering - Concentrate on beacon chain pyspec, currently - But should be applicable for Distributed Protocols, in general - E.g. network layer (libp2p), other blockchains, oracles --- ## Key problem Expressive language means it's more difficult to reason about. ==> S/W engineers and FM practioners chase different goals, as a consequence. --- ## Key problem Beacon chain perspective - Formal Methods importance is recognized - But the spec development process is centered around traditional S/W engineering ==> FM practioners needs are largely ignored. My research tries to answer "What can be done about it?" --- ## Beacon chain problems (FM perspective) - Python is a bad choice from FM perspective - lack of tools, semantics, etc - pyspec is not a spec - not only from FM perspective - pyspec is a moving target - syncing can be costly - manual implementations in different languages - easy to introduce bugs --- ## Opportunities Good stuff - EF team is open to suggestions (but won't blindly accept them) - FM importance is generaly recognized - Can introduce simplifying assumptions - Transpilation is not crazy difficult --- ## My approach - "Engineer" the spec - Meta-programming - Tailor FM to match problem domain - Light(er) weight formal methods --- ## Engineer the spec - A spec is arguably the most important artifact - Especially true for the beacon chain case - "Engineer" the pyspec to make it suitable for applying FMs (and reach other goals) - most part of the spec is executable - pyspec - Define requirements for the spec - what does "good spec" mean? --- ## Tailor FM to problem domain - Constrain expressivity but gain simpler formal reasoning - Python subset employed by the pyspec is already restricted - type annotations, limited OO features, limited set of types, no concurrency - Simplified memory model - mostly about restricted aliasing --- ## Meta-programming - Transpile pyspec to a "better" form - pure functional - for formal needs - other langs - for more practical stuff - Executable semantics for a subset of Python - Pehaps, other execution models: - Extensions of Datalog - Differential dataflow --- ## Light(er)-weight FMs - Start from light-weight formal methods (static type checking) - easier to introduce - less annotations (easy to adapt to changes) - still useful - Continue with middle-weight stuff - extended static checking - bounded model checking - concolic execution - But aim at full-blown verification in a long term --- # Current state --- ## Transpilation - Semi-automatic translation to Kotlin - Regular pyspec updates (phse0/phase1) - Used as a base for Mikhail Kalinin's work on Eth1/Eth2 simulation - Several pyspec bugs found+fixed - Working on dataflow analyses - to support translations - starting point for semantic work - Working on a translation to Rust --- ## Research stuff Mostly ready, but not published yet - [Formal Engineering for Blockchains, part 1](https://hackmd.io/REqkGV21T8Kf86Rh_FFN_g) - [Formal Engineering for Blockchains, part 2](https://hackmd.io/mq7a6mOPTYacVux7fssL-Q) - [Formal engineering of beacon chain spec](https://hackmd.io/29oG2wvORLmUekkPnhOjpw) Started to work on "semantics" - typing rules - memory model --- # Plans --- ## Near term plans - Complete dataflow analyses - Fully automated translation to Kotlin - Complete translation to Rust - Implement executable semantics - typing rules - memory model (based on Rust's one) - Spec purification - Pure functional/logic language target - Static analyses - Switch to datalog engines (Souffle, Formulog) --- ## Longer term plans - Complete Formal Engineering series of posts - Trusted Assumption Base concept - Middle-weight Formal Methods --- # Semantics Highlits --- ## Executable "semantics" "Semantics" - a model which allows to tranform the python subset (employed by pyspec) to a "better" form. - pure functional (Coq, Stainless/Scala, WhyML) - other formal frameworks - mainstream langs (Kotlin, Rust, Scala, etc) --- ## Components - start from annotated Python AST - supported features - infer variable declarations - infer types - resolve ambiguities - type libraries (BLS, SSZ, pylib, etc) - typing rules - memory model --- # Memory Model --- ## Some assumptions - Actor model - Protocol is built around a persistent data structure (e.g. blockchain) - Ignore concurrency (inside an actor) - but should be possible in a safe way (e.g. Rust-style) ==> - Pure functions mostly - But mutation is important for state updates --- ## Formal Engineering perspective - Reasoning about mutation can be way more difficult - Pure code can be way more slow Want the best of both ways, under reasonable restrictions --- ## Aliasing Aliasing is the core problem. Several ways to solve: - detect 'no aliasing' at runtime reference - counting + static analysis (Lean, Whiley) - - avoid aliasing - linear/uniqueness types (ATS, Idris, Mercury, Clean, SAC, etc) - avoid "dangerous" aliasing - e.g. Rust's ownership type system with borrowing --- ## "Dangerous" aliasing - Two or more references pointing to the same location - At least one of them is mutable In a concurrent program, access to the location should be synchronized to avoid a *data race*. Rust ownership type + borrow checker prevents such dangerous aliasing. There's either: - one mutable reference - or multiple immutable references --- ## Reasoning and aliasing Formal reasoning about detructive updates is notoriously difficult for very similar reasons. - Formal properties can be seen as *immutable references* - Aliasing means more info about mutations to be propgated --- ## Memory model Typically, some simplifying assumptions are made. Often it's about restricting aliasing: the less aliasing, the less info to propagate. The Rust memory model is very attractive in this respect: - multiple immutable references constitute no problem, as there is no update possible - any mutable reference is exclusive, i.e. there are no other reference to the location. - the approach works well in practice --- ## Fast and Purious My hypothesess are: - the Rust's memory model fits nicely the beacon chain pyspec - the same is true about Distributed Protocol specs, in general - 'Fast and Purious', both goals are achievable: - fast execution (destructive updates) - translation to a pure code w/o blow-up (mutable references are exclusive) --- # Q&A ---