Skip to content

Instantly share code, notes, and snippets.

@jberthold

jberthold/Day-3.md

Last active January 23, 2023 07:39
Show Gist options
  • Save jberthold/8ce9394ac41af28dec23fb1ffbd6f9ee to your computer and use it in GitHub Desktop.
Save jberthold/8ce9394ac41af28dec23fb1ffbd6f9ee to your computer and use it in GitHub Desktop.
Download ZIP
SPLASH Day 3 Notes
Raw
Day-3.md

Notes at SPLASH 2022 - 20221205-10 Auckland NZ

Wed 7 12

SLE Keynote: Shigeru Chiba, about embedded DSL - libraries as languages

"People do not want to learn a new language but a new library"

  • Language vs Library

    • the era of libraries: people tweak libraries instead of making or modifying languages
    • "any sufficiently advanced library is indistinguishable from a language"

  • transition of what a "library" is:

    • collection (library) of functions

    • "framework" = incomplete application program (of skeletons where users fill out core functionality)

    • EDSL:

      • hides internal state
      • typically looks declarative (as much as possible)
      • rejects illegal instantiations (by way of advanced type checkers)
      • Example: Ruby on Rails (often considered a DSL but is a framework)
    • flexible syntax (-> scala, Ruby) allows for "declarative look"
      • macros, operators with infix or postfix notation (+ free arities)
      • language extensions for custom constructs (HS rebindable syntax)
      • different techniques to address problems with parsing and scoping

  • Looking at Python DSLs: PyTorch vs TensorFlow

    • tensorflow loses (in opinion-leader's eyes) for being compilation based, PyTorch "allows for python control flow statements
    • question of embedding

  • Talking about errors (!)

    • from the "Language" perspective, many things should be syntax errors (but are coming out as semantic - type- errors)

    • verbosity can be reduced by generating types from a grammar

    • review of different techniques to chain types for syntax emulation

  • Questions:

    • Libraries vs. languages: languages can restrict usage, while users can always break out of a library
    • What should the host language have to accommodate DSLs well?
      • extensible syntax
    • comment/warning about pitfalls (like parsing ambiguity) to achieve user-friendly syntax
      • "pluralism of languages" preferred (+ fashions are good to shake out bad ones)

FTSCS session (time and state)

Rewriting Logic for Parametric Timed Automata

  • Background: 1) Parametric Timed automata 2) Maude and Rewriting

    • timed automata: reachability problems + parameter bounds checking
      • solved using "parametric time zone graphs"
    • Rewrite theory (mini-intro to Maude)

      • to model the coffee maker automaton

      • NB: passage of time is manual, model carries many parameters

  • This paper: Proposes systematic translation from PTA to rewrite system

    • Proof of soundness in paper
    • tool for searching particular constrained states
    • parameter synthesis (as a reachability problem)

"Q: A Sound Verification Framework for Statecharts and Their Implementations"

  • (Sandia Labs work, for "high-consequence embedded control systems")

  • large concerted and controlled effort to create a consistent framework for development,

    • SW/HW coherence ensured, formalised (but at times poorly tool-supported) development process, test and proof methodology supported by model checking (NuSMV),

  • Treatment of C code

    • Clang-based annotation of C with its ACSL spec,
    • translation to CLight and back, to ensure constrained style and guarantees) (-> CompCert, -> FramaC)

  • Tool to connect all spec (just doc.s) with state model and code

  • ..

SLE session about Verification, Validation, Testing

Lang-n-Prove (Virtual talk)

  • interested in how proofs in proof-assistants can be made into schemas

    • lang-n-prove expresses "language proofs" (for classes of languages)

    • target languages:

      • requires clear identification of introduction and elimination forms
      • current evaluation: "variety of functional languages"

    • slides contain language syntax and various examples illustrating how the proof gets applied to different cases in a prototypical language

Property-Based Testing: Climbing the Stairway to Verification

  • idea/message: combine Cogent and property-based testing towards verification

    • Cogent: specialised language amenable to system verification
      • strongly typed functional
      • proofs in Isabelle (embedding), compiled to C + refinement
      • proving stepwise data refinement (over relations, allowing for non-determinism via existentials)
    • to add PBT, replace the Isabelle embedding by a HS embedding
      • and add tests rather than a proof of the refinement

  • Benefit: low-effort -> reasonable assurance without a full proof

    • can gradually prove components while using PBT for others

    • particularly relevant for maintenance, when making changes to the proven program or to the Cogent ecosystem (recurring manual work required for Cogent is required for parts of the system)

  • Questions:

    • The PBT approach breaks down for things that are not executable
    • (concretely, the refinement of relations requires relations to be executable)
      • Answer: this is for the input relation but the output relation does not need to.

FTSCS Workshop, Applications session

Modelling a Blockchain for Smart Contract Verification using DeepSEA

  • based on the Certik work
  • deepSEA approach and pipeline: see screenshot
  • goal of this work:

    • provide a blockchain model (cohesive as a whole), as opposed to proving refinement of individual contracts

    • main contribution: "Successful-calls approach", focusing on the happy path(s) of contracts.

      • In the model, each call needs to be accompanied by a proof that the call will succeed. (- Compilation chain: deepSea -> Coq -> Solidity)

Successful calls approach

  • individual Coq models generated from a graph of possible actions (assumed to succeed)
    • actions type, requires prior blockchain state to formulate success lemmas for the possible actions
    • step function..
  • example (crowd-funding): see screenshot
    • successful-calls approach removes clutter from the proof, by introducing required conditions automatically.
  • limitations:
    • dependent pair (state, actions) required for successful-calls
    • handling the case for revert (by making it its own action)
  • Questions:

    • successful-calls approach ignores cases where the contract is unable to make any state change action (think DoS attacks)

      • such a DoS state would have to be reached through a successful action, the method would have means to reason about this case.

    • Encoding of actions specific to contract. how about interaction between two contracts?

      • currently actions hand-written but goal is to gemerate. This generator should consider contract interactions.

(Towards a) Formalization of the Active Corner Method for Collision Avoidance in PVS

  • work in progress

  • setting: issuing commands to pilots to avoid mid-air collision

    • previously proven by a geometric argument, now using a more symbolic approach
      • trade-offs in either direction
    • goal here: bridge the gap and automate part of the work upfront

  • method: "follow the corners" to define a safe/unsafe polygon

  • highly problem specific results, proposing a methodology to compute regions from a moving convex polygon in 2D.

  • ideas (this is WIP) for generating/including proof certificates, since the implementation is python

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment