SPLASH Day 6 Notes

Day-6.md

Notes at SPLASH 2022 - 20221205-10 Auckland NZ

Sat 10 12

Keynote : "I can get no - Verification"

(Atsushi Igarashi)

Intro

• SW verification as "the holy grail" (Bill Gates, 2002) is within reach today (Gates claims that in 2002 for device drivers)

• but still we are busy developing verifiers every day

• will talk about smart contracts, IoT, research directions and current development

  

Two application areas

Smart contracts

• challenges in smart contract verification: invocation of other, unknown, contracts (-> verification of HOFs), unclear spec.s

• setting: Tezos BC, Michelson language (functional stack-based with blocks, rich set of primitive types)

  • Michelson for smart contracts: stateful, continuation-style (no return as such), no (direct) operation to invoke other contracts

• own work "Helmholtz" (observing Michelson!)

  • verifier of Michelson contracts
  • hard-wired variables amount,ops,source in pre/post-conditions
  • background: refinement types, adapted to HOF stack-based languages
  • implementation: no surprises, using an SMT solver on the computed strongest post-cond.

• Experience:

  • building a verifier from scratch, cumbersome
  • single contracts are not interesting, contract interaction is what implements interesting use cases
  

• Verifying multiple contracts

  • "Dexter" (decentralised exchange) as a case study
  • tokens as a derived currency, using a constant Product Market Maker (CPMM) together with the token holding account
  • transfer and approval (of an allowance) calls
  • CPMM: can sell tokens for XTZ on behalf of account owners
    • (several mistakes on the slide!)
  • example of CPMM interactoin to exchange tokens for tz
  • two flaws:
    1. allowance setting allows tokens from Alice to be stolen
       • when allowance is set, anyone can step in to make CPMM transfer
    2. anyone can steal from CPMM
       • self-transfer must succeed, so X=CPMM allows anyone to steal
  • proposed solution: remove XferTokens first parameter (-> screenshot)
    • insufficient and going in a wrong direction
    • Helmholtz-based invariants proposed to fix the CPMM flaws

• to summarise:

  • verifiers are not easy to build, more support from PL community
  

Zero-trust IoT project

• goal: verify protocols and trust chains (static + dynamic)

• "DevSecOps" (buzz buzz buzz)

• Experience:

  • IoT system verification is hard, even for experts
  • example: a published paper turned out to make impossible assumptions (turning on a device more than once)
  • verification tools should be usable by IoT System dev.s (but aren't)
  

• Questions

  • about the boomerang example, infinte loops: prevented by gas consumption
  • analysing instruction output vs. interprocedural semantic analysis
    • problem 1: unknown contract may be invoked
    • problem 2: instruction list may be long (and execution may fork)

Concurrency session

A Concurrent Program Logic with a Future and History

(Roland Meyer)

• applying separation logic to data structures in concurrent programs

• two challenges: concurrent unbounded updates, linearisability

• unbounded updates: example of removal

  • recursive SL predicates and induction hard to automate
  • "ghost update chunks": composing updates
    • can be composed during the program traversal without overhead
    • walk through an example.. (screenshots)

• Linearisability

  • example: containment in a list in the presence of concurrent removal
    • possible to linearise concurrent actions to consistent sequence
  • proposal: "past reasoning" about interference
    • concurrent interfering actions are not able to change the past captured in the traversal

• both proposed concepts formalised in separation logic, with an implementation of proving several challenging examples

  

CAAT (Consistency as a Theory)

(awarded paper, Thomas Haas)

• "theory and solver for weak memory"

• Motivation: ways to find bugs in concurrent programs

  • using bounded model checking etc.
  • with the help of a SAT solver
  • neglecting the fact that threads communicate (over shared memory)
    • requires a memory model, and to include it in the model/SAT solving

• What are memory models?

  • examples: Seq. consistency, total store ordering (buffered write-back)
  • can be described by CAT (DSL describing consistency models)
    • uses a number of base relations and derived relations to describe consistency-related properties of operations
      • po = program order, rf = read-from, co = coherence
  • example: Peterson's Mutex (screenshots)

• encoding memory model descriptions (CAT) into logical theories

  • a number of basic axioms need to be added to a straightfwd encoding
  • problem: recursion in CAT
  • solution: encode CAT as instead of in a logical theory
    • theory only talks about base relations, but considers derived relations internally
    • example (screenshot): happens-before cycle encoded in this theory
  • generalisation possible: abstract base relations (e.g., DB transactions)
  • decision procedure: checking consistency of a conjunction, (provided by a SAT solver), providing explanations for inconsistencies
  • in the example:
    • deriving formulas from the execution trace..
    • discovery of a happens-before-cycle
    • removal of derived relations from explanation
  

Implementing and Verifying Release-Acquire Transactional Memory in C11

• classical example: message passing sync using a variable

  • under C11 relaxed memory model, the sync. may be broken (2nd thread reading a prior value)
  • "release-acquire atomics" annotations to fix this by enforcing a global ordering
  • example2: using CAS instead to attempt a fix
    • C11 manual provides a range of different CAS operations

• this work: generalising the release-acquire idea for CAS

• extensions:

  • transactional read-wrote seqiemces
  • release-acquire transactions (3 threads performing a transitive release-acquire synchronisation)

• Formal semantics (overview)

  • builds on "TMS2" model (memory snapshots based reasoning)
  • extension of the snapshots to indicate release or acquire
  • acquiring transactions must read from releasing ones

• Implementation of release-acquire transactions

  • follows as a modification of prior art (TxRead/Write)
  

Logic and Verification II

On incorrectness logic in quantum programs

• proposes transfer of incorrectness logic to quantum computing setting

• early-stage work to be further generalised, considering quantum-specifics (noise) and local reasoning

  

Weighted Programming: A progr. paradigm for speciying math. models

(Kevin Batz)

• "enable probabilistic programming for programmers inexperienced in probability theory"

  • this work: extends this to the "mathematical theory" as a whole

• proposes "weighting", here extending a prototypical imp language

  • weighting (x) accumulates
  • branching (+) considers two branches (and, e.g., minimises)
  • theory applicable to different settings: optimisation, reasoning about program traces, combinatorics, resource analysis, etc)

• variants of semantics

  • operational: weighted automata - resulting in infinite state
  • denotational: weakest precondition and invariants.
  • one-path search for pre/post-condition correspondence
    • adding weight to the valid final states (true post-cond.)
    • semi-ring sum over all valid final states yields solution

• weakest pre-weightings are synthesised (syntax-driven)

  • (backwards) pushing (n + y) through the example program (screenshot)
  • same for invariants (loop body)

• weakest liberal preconditions

  • accounting for non-terminating programs.
  • adds greatest-fixpoint to inference in the loop statement

• case studies: screenshot

  

Wildcards Need Witness Protection

(awarded paper, Kevin Bierhoff)

• addresses a fundamental unsoundness in Java and Scala, reported in Oopsla16

  • solution along the Oopsla16 paper, with a new example
  • key: typing of null

• wildcards: address invariance of java collections (List(Integer) not < List(Num) not < List(Object)

• wildcards can address this, they instantiate the existential type given in a collection type

  • java aims to ensure these exist, but does not allow for specifying them (no introduction form)
  • elimination form usually exists, too, but again not in Java

• => Java wildcards have lower and upper bound (lower often bottom, upper often Object)

• walk through the types in the example crash

• previous proposal to solve this: limit wildcard subtyping

• here: ensure all wildcards have a witness type

  • which makes an instantiation with null impossible (no witness)
  • explicit elimination of wildcards using a special let construct
  • limiting the type of null to require a witness

• proof of preservation and progress:

  • problematic side is progress proof
  • requires a "witness lemma" to ensure that a witness is available (see null restrictino before)

• evaluated as a javac plugin ("Error-prone") on the google codebase

• enabled by default in Bazel and available as OSS

  

list-of-slide-screenshots.md