![[Home]](http://www.bayleshanks.com/cartoonbayle.png)
---
eth formal verification
swordswinger12 1 day ago
The IC3 research group at Cornell, and especially Elaine Shi's group, has been thinking about this recently. They are (I think) working on some kind of program analysis framework using deep PL techniques to formally verify smart contracts.
reply
pipermerriam 1 day ago
There is actually already fledgling support for this in Solidity (the prevailing language that Ethereum developers use to write smart contracts).
https://forum.ethereum.org/discussion/3779/formal-verification-for-solidity-contracts
---
https://www.reddit.com/r/ethereum/comments/4uu9fb/formal_verification_for_solidity/
" The second iteration of formal verification features for Solidity has been released!
It is now possible to verify re-entrancy effects using invariants!
Listen to a talk about it or just view the slides - the talk includes a live demo that shows how to use the new feature in browser-solidity.
What can be done with it: Not all of Solidity is supported, you will see error messages if you use unsupported parts of Solidity. Basically, the uint type, arrays of it, arithmetics on it, assignments, while loops, if statements, functions, internal function calls (also recursive) and sending Ether via .call.value(x)() is supported.
What is not supported: Function calls to other contracts (apart from sending Ether), the msg and block variables (receiving ether is not yet modeled), mappings, custom datatypes and datatypes other than uint.
How are effects of reentrant calls handled? Any conditions that are used atop of the contract definition are automatically applied to (and verified for) all functions of the contract. For now, you still have to make sure that these conditions are transitive. This means that a condition of the form "the balance increases by 1" is invalid (because two calls will not satisfy the condition) and the system will not yet notice that. In contrast, a condition of the form "the balance will not decrease" is valid.
What are the next steps? The next step is to add support for mappings, so that it is possible to formally verify a simple EIP20 token.
Comments welcome!
"
---
" Animats 128 days ago [-]
The system: [1] The Nelson-Oppen decision procedure: [2]
There's a subset of of arithmetic and logic that's completely decidable. It includes addition, subtraction, multiplication by constants, "if", the theory of arrays, a similar theory of structures, and the Boolean operators (on bools, not integers.) This is enough for most subscript and overflow checks. Complete solvers exist for this subset. If you try to prove all constraints that need run-time checks with this approach, you can eliminate maybe 80-90% of run time checks as unnecessary.
Some checks cannot be eliminated, but can be hoisted out of loops. This means making one check before entering the loop, rather than one on each iteration. FOR statements usually can be optimized in this way. That's almost a no-brainer in modern compilers. The "Go" compiler does this. Heavier machinery is needed for more complex loops.
[1] http://www.animats.com/papers/verifier/verifiermanual.pdf
[2] http://www.cs.cmu.edu/~joshuad/NelsonOppen.pdf "
links 2 abstract:
A method for combining decision procedures for several theories into a single decision procedure for their combination is described, and a simplifier based on this method is discussed. The simplifier finds a normal form for any expression formed from individual variables, the usual Boolean connectives, the equality predicate =, the conditional function if-then-else, the integers, the arithmetic functions and predicates +, -, and _<, the Lisp functions and predicates car, cdr, cons, and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. If the expression is a theorem it is simplified to the constant true, so the simplifier can be used as a decision procedure for the quantifier-free theory containing these functions and predicates. The simplifier is currently used in the Stanford Pascal Verifier. Key Words and Phrases: program verification, program manipulation, theorem proving, decidability, simplificatio
---
i guess for Oot it would be coolest if we could define ASSERT in terms of a statements that meant "(at this point in the program) (EXPRESSION) is true", eg if the noun phrase "this point in the program" were reified and if the phrase "at this point in the program" were reified, so then you could use the ordinary logic programming syntax to say "EXPRESSION is true"
---
verification:
https://isabelle.in.tum.de/overview.html
---
mentions
---
" Let us assume that you have a correctly implemented token contract with a total supply of 1000000. Then whatever function you call, the sum of all tokens will always be 1000000. Your contract would look something like (only sketching here)
/ @why3 ensures { sum (old this.storage.balances) = sum this.storage.balances } contract Token { mapping(address => uint) balances; function transfer(address to, uint amount) { ... } }
"
---
maybe the terminology should be 'requires' and 'ensures'
eg:
https://chriseth.github.io/notes/talks/formal_ic3_bootcamp/#/6
---
" Krakatoa and Jessie are two front-ends of the Why platform for deductive program verification. Krakatoa deals with Java programs annotated in a variant of the The Java Modeling Language. Jessie deals with C programs annotated in the ANSI/ISO C Specification Language (ACSL). "
---
why3:
---
http://web.cecs.pdx.edu/~apt//cs510spec/
---
http://web.cecs.pdx.edu/~apt//cs510spec/ :
Tools
Tool Investigation Ideas
---
https://lists.gforge.inria.fr/pipermail/why3-club/2015-October/001308.html lists:
• Concrete knowledge of a formal tool (like Atelier B, Frama-C, SPARK, SCADE, Coq, Polyspace, Z3 or SPIN) is a plus;
---
great looking talk (already added to toreads under 'provers'):
---
www.dwheeler.com/secure-class/presentations/Secure-Software-10-Formal-Methods.ppt
So you want to prove that a program meets a specification…
Often must write program with that goal in mind
Challenges: Pointers & threads
Variable assignment can be handled, but complicates
Loops can be handled, but complicates (loop invariants)
Functional languages common (at least underneath), including Lisp, ML, OCaml, Haskell
Various tools exist that can be used to do this
Already seen tools that can prove programs, including PVS, HOL4, Isabelle/HOL, HOL Light, Coq
Following are some tools (and notations) specifically for it
E.g., ACL2, Toccata/ProVal (Why3), Frama-C + (Jessie or WP), JML (supported by many tools), SPARK, model-checking
As with everything else here, omits much---
" Spec#
public string GetFirstName?(string fullname) requires !string.IsNulOrEmpty?(fullname) ensures !string.IsNullOrEmpty?(return) { return string.Split(” “)[0]; } "
---
Ericson2314 3 days ago [-]
Huh tactics are pretty great. Say exactly what you want and the computer programs itself!
It's unfair to just compare development time between tactic-generated programs in a dependent language with manually written programs in a non-depenendent language. The end result in the dependent language is much more valuable.
reply
catnaroek 3 days ago [-]
I'm not comparing dependent types vs. no dependent types. I'm comparing higher-order dependent types (Agda, Idris, Coq, etc.) vs. first-order dependent types: https://news.ycombinator.com/item?id=12350147
Seriously, Coq-style proof scripts are utterly unredable when they grow past a certain size. The only way to understand them is to replay them, so that you can see the intermediate hypotheses and goals.
reply
---
catnaroek 3 days ago [-]
Agreed. These days, the most popular dependently typed languages are based on some variant of Martin-Löf type theory, in which arbitrary mathematical propositions are expressible at the type level. I'm not convinced that these designs offer a good power/cost ratio. For example, these languages often have very limited type inference.
In practice, most of the properties that a programmer (rather than, say, a mathematician using a proof assistant) would want to enforce mechanically (say, invariants of data structures) are expressible as first-order statements (lambda-bound variables are never applied). This strongly suggests that the ergonomics of dependent types could be significantly improved by deliberately limiting their expressive power. By the way, the idea isn't new: the Damas-Milner type system, which is most certainly known and proven technology, is a subset of System F-omega's type system for which type inference is possible, at the reasonable (IMO) price of not having higher-ranked or higher-kinded types. A dependently typed language with a first-order type level would benefit from reusing the basic architecture of a Damas-Milner type checker: a constraint generator and a constraint solver powered by a first-order unification engine.
reply
seanwilson 3 days ago [-]
> By the way, the idea of deliberately limiting the expressive power of types isn't new: the Damas-Milner type system, which is most certainly known and proven technology, is a first-order subset of System F-omega's type system for which type inference is possible. A dependently typed language with a first-order type level would benefit from reusing the basic architecture of a Damas-Milner type checker: a constraint generator and a constraint solver powered by a first-order unification engine.
Have you seen languages like DML (let's you capture linear arithmetic properties only and automates the proof of these)?
https://www.cs.bu.edu/~hwxi/DML/DML.html
> Dependent ML (DML) is a conservative extension of the functional programming language ML. The type system of DML enriches that of ML with a restricted form of dependent types. This allows many interesting program properties such as memory safety and termination to be captured in the type system of DML and then be verified at compiler-time.
What program properties are useful to capture and what properties you can mostly automate is a really interesting problem.
reply
catnaroek 3 days ago [-]
> Have you seen languages like DML (let's you capture linear arithmetic properties only and automates the proof of these)?
Yes. But what I have in mind is a little bit more ambitious. I want dependent types restricted to be parameterized by syntactic values (in the sense of ML's value restriction) of what Standard ML calls `eqtype`s. For example, correctly balanced red-black trees would be:
(* clearly eqtypes *)
datatype Color = R' | B'
datatype Nat = Z | S : Nat -> Nat
datatype Tree =
| Empty : Tree (B', Z, 'a)
| R : Tree (B', 'h, 'a) * 'a * Tree (B', 'h, 'a) -> Tree (R', 'h, 'a)
| B : Tree ('c, 'h, 'a) * 'a * Tree ('c, 'h, 'a) -> Tree (B', S 'h, 'a)reply
seanwilson 3 days ago [-]
Any examples? I'm curious for examples of a nontrivial type that would catch lots of common programming errors where the proofs can be automated. I see lots of new dependently typed languages but not much interest in addressing the proof automation aspect.
reply
jroesch 3 days ago [-]
You don't need type theory to verify program properties, people have been using first-order methods for decades to prove properties about programs. For example there was a line of work in ACL2 that verified a microprocessor implementation, as well as plenty of modern work using tools like SMT to automatically prove program properties, see Dafny, F* for language based approaches. Though there is plenty of language agnostic approaches as well. My colleagues at UW have a paper in this year's OSDI verifying crash consistency for a realistic file system with no manual proof.
reply
igravious 3 days ago [-]
If (like me) you didn't know what the abbreviation SMT stands for -- I looked it up and it is Shiver Me Timbers http://encyclopedia.thefreedictionary.com/Shiver+Me+Timbers Seems to be some kind of pirate speak.
Only kidding! It stands for Satisfiability Modulo Theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
“In computer science and mathematical logic, the satisfiability modulo theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on. SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming.”
I'm not sure I'm any the wiser after that …
A notable building block appears to be SMT-LIB http://smtlib.cs.uiowa.edu/index.shtml
reply
catnaroek 3 days ago [-]
Nice. SMT can be (and indeed has been) integrated into type-based approaches to program verification as well.
reply
jroesch 3 days ago [-]
Yeah I think SMT is really the state-of-the-art right now in this area. Leo De Moura (one of the main authors of Z3) has been working on Lean for the past couple of years. There is a small group of us (5~) who have been working on a big release for the past couple of months. The goal is to bring the easy of use of SMT automation to type theory, so you can get both the ability to do induction and automation.
Lean: http://leanprover.github.io/
reply
catnaroek 3 days ago [-]
I wish you guys good luck. Freedom from Coq-style proof scripts should be the goal.
reply
catnaroek 3 days ago [-]
I'd love to give more concrete examples, but I'm slightly hampered by the fact the type system I want isn't actually implemented anywhere. I have a rough sketch of the design of the type system I want, and I've been looking for a computer scientist, logician or mathematician to help me polish the design and prove that it is, in fact, type safe. But I couldn't find anyone. :-
reply
naasking 3 days ago [-]
Why not just learn Coq or Agda yourself? There are also sorts of introductions for simple type systems that I'm sure you can build off of.
reply
catnaroek 3 days ago [-]
I have no idea how to implement fresh unification variable generation (my type system is a superset of Damas-Milner, kind of like how the calculus of constructions is a superset of System F-omega) in Coq or Agda. Everywhere I've seen it implemented, it involves mutable state. So, “in principle”, I could fake it using something like the state monad, and plumbing around the collection of unification variables generated so far, but in practice reasoning about this seems like a pain.
reply
mietek 3 days ago [-]
You could take a look at Coquand (2002) “A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions”.
https://www.dropbox.com/s/xmj7yv1i1moe0ag/Coquand2002.pdf
Drop in to #dependent on Freenode IRC, and let’s chat.
reply
jroesch 3 days ago [-]
Type inference isn't the most important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible. Not to mention you can get pretty good "inference" in dependently typed programming languages just by designing an appropriate higher order unification procedure. I have never met a daily user of these tools that find this to be the bottleneck.
In practice you spend way more time writing proofs in these system then doing anything else. There is evidence that we don't need to limit the expressive power of our logics, just design appropriate automation for the logic. Lean, a new ITT based theorem prover from MSR, has been focused on building automation for type theory. It already has promising results that formal methods techniques can be scaled to type theory (see the website for more information on recent work).
reply
catnaroek 3 days ago [-]
> Type inference isn't important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible.
What I'm saying is that I don't like this direction, because type inference is very important to me.
> Not to mention you can get pretty good "inference" in dependently typed programming languages just by designing an appropriate higher order unification procedure.
Such higher-order unification procedures must always be tailored towards specific use cases, since higher-order unification is in general undecidable. Effectively implementing a different type checking algorithm for every program I write doesn't feel like good use of my time.
What I want is a type system that is more honest about how much it can help me: it only promises to enforce properties expressible as first-order statements, but offers much better inference, and the remainder of my proof obligation is hopefully small enough that I can fulfill it manually.
> In practice you spend way more time writing proofs in these system then doing anything else.
Indeed, and that's what I'd like to fix.
reply
nickpsecurity 3 days ago [-]
I like your proposal of first-order, dependent types. Shocked I havent heard of it before now given advantages. I hope someone helps you build it.
On related note, what do you think about the Shen LISP approach where Sequent Calculus can be used for advanced typing? Does it have the expressibility and decidability benefits you described? Hadn't seen many specialists talk about it so still an unknown to me. If it does, I figure some default type systems could be created for a specific style of Shen and/or specific libraries. Or something similar done in a ML.
http://www.shenlanguage.org/learn-shen/types/types_sequent_c...
reply
---
http://www.seas.upenn.edu/~plclub/poplmark/poplmark.pdf mentions [26], Coq [3], HOL [18], HOL Light [21], Isabelle [35], Lego [28], NuPRL? [7], PVS [40], Twelf
---
" ... program in a language rich enough to express our correctness constraints, our compiler optimizations (§4.1), and the proofs of correctness of those optimizations. Instead of merely packaging up algorithms (which we believe to be correct after careful inspection) into libraries, we can package up correctness criteria and proof tactics into libraries. ...
3 GrayGnome? 2 years ago
| link |
What you say has been a dream of PL researchers for a long time now. Ada 1 is one of many languages that has strong guarantees and static analysis in mind. ACL2 2 was used to verify the correctness of the floating-point unit in the AMD K6 after the FDIV bug was exposed in Pentium processors. However, as we know, verification of certain safety properties is an NP-complete problem. Lighter approaches have been considered. The Eiffel 3 programming language is a strong proponent of design-by-contract where pre and post-conditions of functions are given in the function definition. The Alloy 4 model checker lets you verify abstract models that you design in specifications. Unfortunately, most attempts at model checking, designing by contract, or engaging in strict static analysis, has been met with failure or disuse. A discussion of Coverity’s 5 static analysis tool exposes a lot of the issues that formal verification faces in industry ( http://cacm.acm.org/magazines/2010/2/69354-a-few-billion-lines-of-code-later/fulltext ).
For a look at current projects employing formal verification, take a look at seL4 6 a verified microkernel, Quark 7 a formally verified browser kernel, Jalangi 8 dynamic Javascript analysis, and Ur/Web 9 a web programming language with a strong analysis engine.
"
---
so a potential verification syntax:
LABEL1: ?: n == 1 n = n + 1 !: LABEL1 -> n == 2
we have:
and we could have:
LABEL1: ?: n == 1 n = n + 1 !!: LABEL1 -> n == 2
where:
Loop invariants are just ordinary assertions within loops.
'decreasing' annotations are:
i = 5 while i > 0: !<: i i = i - 1
note that the !<: applies to the enclosing loop
again, '!!<' is a decreasing annotation that should be taken as given
mbnonterminating:
while i > 0: ^mbnonterminating blah
implies: -> forall: @var
eg:
!: @i ((0 <= i) & (i < len(arr))) -> condition(arr[i])
and mb we want a shortcut for pre- and post-condition after all, so we don't have to actually write the labels for pre-conditions, and the implications. Mb use '? condition' for an ordinary hypothetical, and '! condition' for an ordinary assertion, and '?:' and '!:' for pre- and post-?
or mb ?-: and !-: for pre- and post. or ?. and !. for pre- and post-. Or ?> and !>.
---
y'know, my idea that a pre-condition is a hypothetical assertion and a post-condition is an implication involving that assertion isn't quite true; the use of the precondition isn't limited to the postcondition; assertions 'under' the precondition also assume the precondition.
so just use ?: and !: for pre- and post-conditions, or even ? and !
actually mb use ! for assertion, !? for pre-condition, b/c then ? can be used for other logicy stuff, and '!' is for assertiony-stuff.
hypothetical assertions can be ??:, but we probably won't need them, so leave them out for now
---
https://www.youtube.com/watch?v=Nw1glriQYP8&feature=youtu.be&t=1071
---
" I can only think of one tool that can formally verify user generated code (cryptol) and even then it's only for a small subset of C/Java that applies to crypto work. "
---
" > nothing is stopping you from porting your formally verifiable language to Ethereum
I wish this were true but it isn't. We spent months trying to see if there was a way that it would work because we would have preferred this approach. The EVM itself is stopping us (as well as the shape of the Eth blockchain but we could probably have worked around that problem). Pact is interpreted, so while we could make an EVM version technically it's practically unworkable -- there's nowhere near enough gas to run the interpreter. We couldn't compile directly to EVM either as the EVM just doesn't do enough[1] for you. It's closer to a 1980's era CPU ASM than a modern VM (like the JVM). Moreover, the Pact runtime does a lot of things for you (as a safety feature) that the EVM just doesn't have a notion of. Even then, while all of the Pact-compiled-to-EVM code would work and be safe, we couldn't protect it that code from EVM code that doesn't play by Pact's rules. Moreover, supporting all the extra things that Pact does for you would make it, again, run out of gas on EVM.
This discussion is very similar to putting Ed25519 on the EVM. While you can technically implement it in EVM, it's just too gas-heavy. It's best to extend the EVM itself to do more.
That's the thing about having the EVM be Turing-complete, it makes people think that "it can do anything and thus abstracts over the problem thus solving it." This is technically true but not practically true -- all you are doing is punting a huge number problems/required features (like dispatch and module loading) down the road for the language to figure out. In a gas-metered context, every feature the language adds because the EVM lacks it costs gas and thus makes a number of features impossible in practice. "
---
spopejoy 84 days ago [-]
> It sure makes me wonder if Ethereum would do better with a less forgiving programming language.
This will be hard. While Solidity certainly has problems unto itself, some of its insecurity comes from the EVM's design, which is almost laughably low level and thus very hard to reason about. It certainly doesn't seem to be informed by modern VMs like LLVM, JVM or BEAM, which know a great deal more about the semantics of the program they're running and have things like dispatching features. My guess is the approach was "Bitcoin with a few more opcodes" and therefore more like a 80s-era CPU than a "VM".
As a result, the compiler is tasked with running the whole show. Add to this the coupling of RPC to Solidity's mangle-check-and-jump dispatch approach, and you start to see why there's been so little innovation in this area: Solidity has a tight grip on the Ethereum ecosystem. Also, writing a compiler to this substrate is not easy, and you're penalized for code size (there's a limit on how big a contract can be).
I'm opinionated, as an author of a competing smart contract language (http://kadena.io/pact) that runs in an interpreter, is Turing-incomplete, has single-assignment variables etc etc which we think makes a lot more sense for the kind of stylized computing you're doing on a blockchain. We even have the ability to compile our code to SMT-LIB2 for use with the Z3 theorem prover and will be talking more soon about our DSL for writing proofs. Interestingly though, we find that choosing the right domain for your language goes a long way towards safety AND expressiveness, so that you're not constantly cursing your compiler/interpreter while also worrying less about $50M exploits :)
---
still_grokking 83 days ago [-]
Ethereum is a flawed design, no question.
But how does kadena's Pact compare to Ivy[1] by Chain[2]? The goals seams quite similar.
[1] https://blog.chain.com/announcing-ivy-playground-395364675d0... [2] https://chain.com/
---
" Indeed, SQL is Pact's biggest influence. After all, SQL doesn't need Turing-completeness, mutable variables, unconstrained loops. With Pact, we sought to end the war between SQL and stored procedures (most DBs use a different dialect for SPs than SQL) with "one lang to rule them all". "
---
serhei 84 days ago [-]
Heck, the basic methods of writing provably correct programs have been explained in plain English since at least the 70s:
https://www.amazon.com/Discipline-Programming-Edsger-W-Dijks...
https://www.amazon.com/Science-Programming-Monographs-Comput...
This is not some rocket science type verification with a dependently typed theorem prover language, it's fairly simple paper and pencil logic. It should not be hard to adapt it to Solidity specific concepts like running out of gas.
---
DonbunEf?7 84 days ago [-]
The original smart-contract language, E, is almost nothing like Solidity. To focus on Turing-completeness, it's true that E is Turing-complete and has an `eval()` primitive, which normally would be dangerous. However, E both comes with sufficient tools to prove that any given instance of `eval()` is safe, and also to limit Turing-complete behavior when needed.
Specifically, in E and Monte, we can write auditors, which are objects that can structurally prove facts about other objects. A common auditor in both languages is `DeepFrozen?`; writing `as DeepFrozen?` on an E or Monte object causes the `DeepFrozen?` auditor to examine the AST of that object and prove facts.
There's a Monte community member working on an auditor for primitive recursive arithmetic, inspired IIUC primarily by the EVM's failings.
The DAO hack happened because of a bug class known as "plan interference" in the object-capability world; these bugs happen because two different "plans", or composite actions of code flow, crossed paths. In particular, a plan was allowed to recursively call into itself without resetting its context first. EVM makes this extremely hard to get right. E and Monte have builtin syntax for separating elements of plans with concurrency; if you write `obj.doStuff()` then it happens now, but `obj<-doStuff()` happens later.
So, uh, yeah. Smart contracts aren't a bad idea, but Ethereum's not very good.
Animats 84 days ago [-]
That's a classic form of GUI bug. Some widget calls something which calls something else which eventually calls the original widget, which is not in a stable state. Classic bugs in this area involve using "save file", and then "new folder", and then renaming some folders in a way which invalidates something upstream.
socrates1024 83 days ago [-]
Do you think it would be possible to improve the EVM by adding E's notion of concurrency? One constraint would be the need to have deterministic scheduling, since every execution would need to be run identically by all validating nodes.
[edit] Incidentally, we pointed out several lessons from the ocap community in a commissioned report from Ethereum foundation back in 2015. Few of those suggestions were adopted at the EVM level or the higher levels though. https://github.com/LeastAuthority/ethereum-analyses/blob/mas...
drdeca 83 days ago [-]
Is this the language E you are referring to : https://en.wikipedia.org/wiki/E_(programming_language) ?
I hadn't heard of it. It sounds neat
---
" It follows that the language that is used to write them should use every known mechanism to discover such errors early. This includes strong typing, immutability, explicitness, design by contract etc. "
---
munin 68 days ago [-]
You could take inspiration from a system like Dafny or F-* and write your contracts with the assistance of a type system and compiler that generated proofs that your contracts satisfied some postcondition given a precondition. People have already written moderately complicated applications like operating systems in these languages, so there's some evidence they could be applied to contracts on the blockchain.
---
" I'm pretty sure that MOST research on program verification has been done in the context of Turing complete systems, from the work of Floyd and Hoare, to the symbolic execution of Deutsch and King, to temporal logic, TLA+, etc. "
---
grogenaut 63 days ago [-]
I'm not sure static typing is tied to formal verification. In fact if you think about it most proofs are basically typeless I a lot of cases.
Cybiote 63 days ago [-]
Dependent or even refinement type systems are where a great deal of research into proof carrying code is done (for refinement types, since systems are restricted to decidability, the proofs are automatic but more limited).
seanwilson 63 days ago [-]
What proof systems are you thinking about? Strong static types seem the most natural way to introduce formal verification into mainstream programming to me.
tom_mellior 62 days ago [-]
(Not the parent here.) ACL2 is a prominent example of a proof assistant without a strong static type system; its object language is a pure subset of Common Lisp. The lack of static types is one of the reasons I find proving in ACL2 to be painful, but others have done amazing stuff with it.
grogenaut 63 days ago [-]
Well general mathmatecial proofs or TLA+... or would it be better to define "integer" as a strong type which I'm willing to concede.
seanwilson 63 days ago [-]
I don't feel there's much difference between e.g. the Coq way where types are used to bake specifications + proofs into the program and the Isabelle way where you write a program with less complex types and prove properties about the program after the fact.
General mathematical proofs? If you mean paper proofs they wouldn't be considered formal as they don't go down to the axiom level.
UncleMeat? 63 days ago [-]
Type checking can be represented as abstract interpretation. It is the mostly widely used kind of formal verification that exists.
---
ekidd 63 days ago [-]
Corecursion and codata are cool, and I would trust Solidity vastly more if it were a "total" functional language with no mutable state and aggressive type checking. Or if it were something more like https://www.idris-lang.org/ , where I had abundant tools to rigorously prove that nobody could steal my money.
Basically, if I'm going to spend even 5 minutes playing with smart contracts, I want to feel like the language designers were incredibly paranoid and aware of just how good modern languages can be at provability and security.
mbrock 63 days ago [-]
If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL.
But, I mean, there's no proof that the Idris compiler does what it's supposed to do, so you'd still have a huge trusted base.
ekidd 63 days ago [-]
> If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL.
Yeah, all my formal proof experience is with Coq, which is just a bit too idiosyncratic and difficult for this sort of thing. But I seem to remember that—especially if you're willing to certify specific results, and not necessarily the program in general—you can make your trusted computing base very small indeed.
I mean, if the CompCert? C compiler can be as thoroughly verified as it is (http://compcert.inria.fr/compcert-C.html), there's no reason why it shouldn't be possible to verify smart contracts.
mbrock 63 days ago [-]
Some pointers you might appreciate:
Jack Petterson and Robert Edström did a master's thesis about retargeting the Idris compiler to emit EVM code, with a custom effect type to express smart contract effects. They ended up modestly skeptical of functional programming as a paradigm for EVM, instead looking toward process calculi. https://publications.lib.chalmers.se/records/fulltext/234939...
Yoichi Hirai's summary of his research into Ethereum formal verification as a full-time formal methods researcher at the Foundation: https://github.com/pirapira/ethereum-formal-verification-ove...
See especially his formalization of the EVM as Hoare triples in Lem, which is usable from Isabelle: https://github.com/pirapira/eth-isabelle -- very cool stuff, although I have to say that the ostensible complexity and difficulty of his proof verifying an utterly simple wallet contract makes me a bit skeptical of this approach to smart contract correctness: https://github.com/pirapira/eth-isabelle/blob/master/example...
seanwilson 63 days ago [-]
> I mean, if the CompCert? C compiler can be as thoroughly verified as it is (http://compcert.inria.fr/compcert-C.html), there's no reason why it shouldn't be possible to verify smart contracts.
Hmm, so from the smart contract examples I've seen, I would have thought writing them in something like Coq would be quite feasible. The code examples I've seen tend to only have simple loops if any, basic conditions and the code is short (e.g. compared to something like web development or mobile apps). Writing anything inside a theorem prover is very challenging though but it seems a compelling application.
If you were implementing a smart contract in something like Coq, I'd be interested to read about what kind of specifications you would typically want to verify. I guess properties like "the owner of this wallet cannot be changed" and "the owner of this wallet can only accept money but not give it away" would be good ones.
---
sounds like Coq and Isabelle are frontrunners for verification systems; agda and idris are talked about a lot
also toread: http://www.cis.upenn.edu/%7Ebcpierce/sf/
---
" Clojure 1.9 introduces two major new features: integration with spec and command line tools.
spec (rationale, guide) is a library for describing the structure of data and functions with support for:
Validation
Error reporting
Destructuring
Instrumentation
Test-data generation
Generative test generation
DocumentationClojure integrates spec via two new libraries (still in alpha):
spec.alpha - spec implementation
core.specs.alpha - specifications for Clojure itselfThis modularization facilitates refinement of spec separate from the Clojure release cycle.
"
https://clojure.org/about/spec
https://clojure.org/guides/spec
https://github.com/clojure/spec.alpha
https://github.com/clojure/core.specs.alpha
---
