~/talk

Cost Analysis of Smart Contracts via Parametric Resource Analysis

on YouTube 34m
Talkat SAS 2020 · 2020-11-18..11-20· [smart-contracts]

speaker

name:Manuel Hermenegildo
links:none on file

resources

video:https://youtu.be/vCraS0-908A
slides:none on file

summary

Claims a reusable method that automatically infers safe parametric bounds for gas and storage and delivers concrete formulas by translating contracts to Horn clauses and solving recurrences. Implements a parametric resource analysis inside CiaoPP, compiles Michelson to CHCs via partial evaluation, attaches a Tezos gas model, and produces bounds like log(A)^2+2B for examples. Analyzer runs in reasonable time, handles Carthage and Delphi models, and updates to new Tezos protocols by changing cost assertions in hours.

AI-written summary · about

chapters (19)

  1. 0:00Cost Analysis of Smart Contracts via Parametric Resource Analysis
  2. 1:15Smart Contract platforms, Resources. ... and Static Analysis
  3. 2:26Challenges and the Parametric Resource Analysis approach
  4. 5:23Resource Usage Analysis - Some Characteristics and Challenges
  5. 6:51Parametricity in the Resource Analysis CLP OY, Bytecode 09 1. Programmer defines the resource consumption for basic elements
  6. 8:54Static Resource Analysis in CiaoPP (Example)
  7. 11:18Static Resource Analysis in CiaoPP - Overview (classical)
  8. 14:09PLAI (CiaoPP's Generic Al Framework) Generic framework given P (as a set of CHGS) and abstract domain(s).
  9. 16:26Resource Analysis within the Abstract Interp. Engine TPLP 14
  10. 17:44Supporting Different Languages & Compilation Levels
  11. 19:12Transformation example - binaries Xcore ISA Example
  12. 20:26Energy Usage Verification
  13. 21:31The Case Study: an Analyzer for Michelson Gas and Storage Applying the method and the CPP analysis tools to Tezos contracts
  14. 22:20The Michelson language
  15. 25:56Michelson to CHC IR Translation: Transformations
  16. 29:31The Tezos/Michelson Gas Model: Encoding
  17. 30:05Performing the Analysis
  18. 30:45A Simple Michelson Contract Example (arithmetic): Gas Analysis Results
  19. 32:59To conclude

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.