Skip to content

Instantly share code, notes, and snippets.

@jberthold

jberthold/Day-5.md

Last active January 25, 2023 04:13
Show Gist options
  • Save jberthold/1d547c28086817675af5acd486b2c6ee to your computer and use it in GitHub Desktop.
Save jberthold/1d547c28086817675af5acd486b2c6ee to your computer and use it in GitHub Desktop.
Download ZIP
SPLASH Day 5 Notes
Raw
Day-5.md

Notes at SPLASH 2022 - 20221205-10 Auckland NZ

Fri 9 12

Random notes

  • conversation about debugging (R. O.Callahan):
    • omniscient debugging for Haskell
    • limited history for a debugger? (back-steps)

Keynote: Improving the Quality of Creative Practices with Pattern Languages

(Takashi Iba)

The world of pattern languages (design patterns etc.)

  • "pattern" taken more generally (origins: architecture) as a description of principles and schemas that have proven useful in a domain. ("rules of thumb" drawn from experience)

  • in SW design: from 1980 (oopsla paper in 1987, Gamma et al)

    • broad up-take, many conferences and workshops arose

  • in SW development process: the Scrum book (and more)

  • Christopher Alexander (architect), origins of patterns, invited keynote at Oopsla 1996

  • Fundamental description of a pattern:

    • Context, Problem, Solution, Consequence
    • "a collection of patterns (pattern language) is required to achieve good overall solutions"
    • (speaker has created over 90 pattern lang.s with >2k patterns, in various domains, most of them not in SWE)
    • This is a "book shop talk"

  • the process of creating a pattern language (created by Iba)

    • roughly: mining, writing, symbolising
    • each with several sub-steps. symbolising = presentation-oriented
    • well-received, described in several books (about SW and game design)

Pattern development in practice

  • again the four elements of a pattern, with presentation (name, picture)
  • various examples of the method being used (pattern cards used to instigate dialogue, etc)
    • practical test.. (in our case, acting just as initial ice breakers)
  • experiences reported: most contexts = early university education
  • examples of pattern languages
    • presentation patterns (see above)
    • living with dementia, - Book about Dementia
    • inquiry-based learning, active learning
    • life transition (and other advice literature)
    • architecture, marketing, management, etc

How to create a pattern language

  • pattern mining

    • classical brainstorm process (describe, compare, cluster, extract)

Paper: "Le Temps des Cerises" (awarded paper)

Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities

(Aina Linn Georges)

  • decomposing the machine code into different parts exercising fine-grained memory access using individual capabilities

  • capabilities have managed scope (local/global) and lifetime

  • description of potential illegal stack accesses that this work should prevent

  • comparison to closely related work..

  • Key ideas:

    • return capability, encapsulating old SP and continuation (can only be jumped to, not read from)
    • restrictions implemented using invariant older-frame => lower-address
    • several different aspects of access (scenario: untrusted caller calls trusted callee, protection both ways)

  • claim: possible to implement hardware support for this access control

Blockchain session

Elipmoc: Advanced Decompilation of Ethereum Smart Contracts

(Sifis Lagouvardos, company Dedaub)

  • "Elipmoc" = compiling backwards

  • motivation: reify concept of variables and types that is lost in bytecode

    • why not analyse solidity? Often not available, versioning is a problem, widespread use of inline assembly in deployed contracts

  • example of a simple ethereum contract, and its (disassembled) bytecode

  • decompiler: reconstructs structured intermediate code (3-address here) from low-level bytecode

  • pipeline overview: constructs basic blocks and jump structure (as long as static), public entry points, analyse context sensitivity to identify and understand block reuse

    • TAX output = block summary

  • new contribution here: context sensitivity improved by changed algorithm (Transactional sensitivity), other small changes to improve result

  • Transactional sensitivity

    1. "sticky public function context"
    2. n most recent likely function call/return sites
      • leaving the stack with other jump destinations (call)
      • (somewhat) inverse criteria (double pop) to identify return blocks

  • block reuse by the compiler massively complicates matters

  • function reconstruction: not detailed, see slide

  • evaluation:

    • compared against Gigahorse (predecessor) and Panoramix (leading decompiler in industry)

  • Questions

    • ethereum compiler output vs arbitrary bytecode
    • is there an API for intermediate results?
      • just source code (gigahorse)
    • what are the limitations, why not 100%
      • (usually) scalability problems in the algorithms used

SigVM: Enabling Event-Driven Execution for Truly Decentralized Smart Contracts

(Sidi Mohamed Beillahi)

  • targeting the event aspect of blockchain contract execution

    • events purpose: off-chain information about on-chain state changes
    • cannot (directly) be observed by other contracts
    • current mechanism: off-chain relay to feed back event information

  • example: MakerDAO collapse

    • MakerDAO implementation is a set of contracts and a price oracle, propagated through a relay server
      • 20 March 2020: price drop, updates delayed by network congestion, exploited
    • other example: Augur, using a 24h "watchdog"

  • This work: proposes an "event-driven execution" extension to EVM

    • native support for event-driven execution
    • evaluation of expressivity, overhead, gas consumption

  • implementation:

    • signal event primitive
    • contracts can implement handlers for specific signal events
    • "handlers will be executed automatically when the event is signalled"

  • "contracts may need some buffer period before reacting.."

    • proposal to allow for such delays in the runtime system

  • new incentive mechanism for signal transactions

    • who should pay the gas?
    • signal emitter should not have to pay.
    • the handler owner pays the gas.
    • contracts can detach handlers dynamically

  • needs to incentivise miners to prioritise signal transactions over regular transactions

  • other mechanisms proposed to restrict callers (for a period)

Logic and Verification 1

Finding real bugs in big programs with incorrectness logic

(awarded paper, Quang Loc Le )

  • Pulse-X tool, "proves presence of bugs"

  • bullds on prior work that led to Facebook's "Infer"

    • Infer over-approximates behaviour => false-positives
    • other predecessor under-approximates => can always report positives
    • scalability issues in under-approximation
      • -> bi-abduction

  • this work: combining the two

    • compositional under-approximation
    • example of an incorrectness-triple

  • compositional bug reporting

    • if problems are input/argument-dependent:
      • existing approaches use heuristics or user annotations (many false-positives)
      • this work: distinguish manifest or latent bugs in the analysis of the function -> use in caller's analysis

  • compromises between speed and precision for the tool

    • function pointers and unknown functions, incomplete SAT solving

  • evaluation: (OpenSSL + 8 FB-maintained open-source C++ projects

    • comparison to Infer, on older OpenSSL: better fix rate, fewer bugs (but fewer false-positives)
    • newer OpenSSL: better results for Pulse-X

  • Questions:

    • how to handle loops:
      • currently just unrolling the loop - under-approximation
    • Can I configure the tool to not have false-positives?
      • depends on SMT solver, has to avoid function pointers and other unsupported features

Fractional Resources in Unbounded Separation logic

(Thibault Dardinier)

  • one of the Viper makers

  • separation logic by example

    • associates permissions with heap locations
      • creator has full permissions initially
      • permissions are fine-grained, per heap location
      • requires/ensures on methods describe their behaviour wrt. heap locations
    • read/write should be distinguished. solved by fractional permissions
    • permission state extended by a Q ∪ (0, 1] component

  • fractional resources example, illustrating split/combine and application to parts in a recursive procedure

  • this work: establishing foundations of practical split/combine in Viper and other tools

    • semantic multiplication vs syntactic multiplication
    • example of multiplication varieties
      • problem arises from aliasing in data structures (* forbids overlap in the formulas shown)

  • presented work closes an important gap in practical provers using syntactic multiplication: foundations for the "magic wand"

  • "Unbounded" separation logic = temporarily relaxing state bounds in the assertion logic, to allow for composition that visits out-of-bounds states, fixing (reimposing) bounds when recombining

  • Questions:

    • what happens if the 1-threshold is dropped?
      • we lose the frame rule (ensures exclusive access to resources)

Effects session

Effects, Capabilities, and Boxes

(Jonathan I Brachthäuser)

from scope-based reasoning to type-based reasoning and back

  • Setting: System-C

  • motivation: syntactically clarify the scope of exception handlers by an explicit name

    • screenshots: comparing System-C and the proposed approach, for rethrow

  • traditional effects vs capability-based effects

    • traditional: conservative approximation on occurrences, dynamic scope, "type-based reasoning"
    • capability: constraint on the context of statements, conservative approximation of observed (handled) effects, lexical scope

  • effect safety with capability-based effects

    • closing over capabilities
      • enables effect polymorphism, breaking effect safety (handlers gone)
      • proposal: use 2nd-class values (Oopsla16) to forbid closure
        • function signature with effect parameters (2nd class)
        • drawback: no 1st-class functions with this approach
        • this paper: removing this restriction

  • tracking more details of 2nd-class values, then using boxes to bridge between 1st and 2nd class values

    • typing formalism: screenshots (details of 2nd-class values)
    • boxing: explicitly wrapping HOFs with their required capabilities
      • unboxing required to apply the function
      • cannot unbox functions that require capabilities out of scope

First class names for effect handlers

(Youyou Cong)

  • approach: structure several handlers of the same type with naming

  • applications (by example)

    • (implementation: Koka, using fun for tail-returning methods)
    • example with files: shows handlers are 1st-class
    • example with references (..)
    • neural network example

  • solving the name-escaping problem: Rank-2 polymorphism

    • "scoped effect", preventing effect handlers from escaping
    • examples revisited

  • Questions/Discussion:

    • Contrasting this with the previous talk (same solution, different path)

Systems and Verification session

Linear Types for Large Scale Systems Verification

(Andrea Lattuada, ETH)

  • verified a large-scale system using Dafny

    • issues when reasoning about memory in the SMT solver

  • Dafny intro (-> screenshots)

    • framing conditions vs logic errors

  • observation: framing conditions/invariants accumulate to substantial size in larger systems

    • solution: linear types to express ownership (and prevent aliasing)
    • SMT solver sub-system profits from a linear type system

  • introducing 2 new variable usages to (linear) Dafny

    • shared: can be duplicated and compiled
    • linear: can only be compiled
    • allows for more efficient code, prevents the aliasing error shown in the example
    • shared read usage is possible thanks to an implicit borrow of the linear variable

  • what if aliasing is inherent in the data structure?

    • non-linear data inside linear data: Regions
    • linear inside non-linear data: Borrowing (no runtime checks required)
    • (NB this allows for incremental conversion to using linear types)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment