Byzantine Fault Tolerant Raft With Smart Contracts | Hacker News Reader

Byzantine Fault Tolerant Raft With Smart Contracts

github.com

71 pointsluu19 comments

This and related code bases (such as the programming language hopper, which is my focus) are the work of several colleagues along with myself. Happy to try to answer any tech/computer science focused questions.

NB: a lot of the stuff still has much work to be done, but we're transitioning to working in the open :)

If one of the nodes goes rogue and tries to flood the network with noise, how does the system prevent denial of service?

Author of Juno here -- surprised to see this on here at all given that I didn't tell anyone that it went open (was saving it for tomorrow). I'm losing out on all this sweet sweet karma </s>.

Anyway, to your question (carter focuses on the smart contract language, not the consensus layer): This is actually a semi-normal/expected thing in the case of a network partition. Say one node gets cut off, transitions to a candidate and achieves some high term (but potentially has an out of date log index). When it comes back online/partition ends, it will start spamming the rest of the cluster requesting votes.

What protects the rest from this or other faults is a combo of signed RPC's and extra logic (i.e. lazy votes). With sigs, chatter from someone who you don't have the key for (or invalid msgs generally) just get dropped + authorship is verified (Follower can't pretend to be some other node). With lazy votes the portion of the cluster in a good state basically chills (stays in same state, doesn't vote) until the Followers hit an election timeout (AE clears the lazy vote).

Of course you can still DoS the NIC or Haskell server, but the important thing to note is that this isn't meant for a public-facing deployment. It's designed for an internal network -or- inter-corp via leased lines/secured pipes setup. That's the whole point of Juno really... for enterprise applications bitcoin-class tech gives you more features than you need (at the cost of performance).

Tangaroa was a great first step, but we have internal fixes for a number of cases it didn't cover, issues caused by incomplete implementations and (I think) some novel ideas to give back... but I'm still finishing the paper on the enhanced/new (not sure what the line for that is) protocol and its implementation so it didn't make the cut for this release.

A better question is: why isn't that network flood tripping all of your monitoring services? :). I'll let the folks who focused on the replication code base address that more

I'm currently focused on the language engineering side (though i was part of the early distributed replication effort, when we ported a verified raft code base to haskell, see https://github.com/cartazio/haver-raft . We ultimately didn't use that code base for a variety of reasons relating to how that verified alg was structured, but all the initial commits should be syntactically equivalent to the coq code in verdi raft, and all the follow on commits should be strictly syntactic transformations. https://github.com/uwplse/verdi is the associated coq development )

Juno follows Raft/Tangaroa in that it treats the state machine like a black box which it runs strictly post-commit.

Significantly, this means it doesn't do a full BFT (which is ultimately application-specific), meaning it is possible to DOS with correct-but-spurious messages.

We are investigating ways to lazily verify SM results, which would necessarily be application specific. This opens the way for an application to code DOS resistance.

This is really neat.

How does a system like Hopper compare to the Ethereum Virtual Machine?

short short answer that is deliberately terse: the hopper language, once a wee bit more mature, will be a dependently type language with linear types (to model first class ownership) and a few other facilities for modelling interaction and authorization along with logical soundness as hard goals. Imagine if agda had a linear logical baby that was designed to be easily embeddable in a host application and/or standalone, and also designed with RTS and compiler improvements from the the outset. plus a few other tbd goodies to make it nice to use.

the ethereum vm doesn't have any notion of ownership or authorization built in, those are provided whole cloth by application level authors (have fun doing that correctly for every app!). I could opine more than that, but I think thats the most i should say about the quality of the stack vm specification or its semantics :)

> I think thats the most i should say about the quality of the stack vm specification or its semantics

As someone who spends a lot of time with Ethereum, I'd love to hear more. Honestly, I almost never deal with the stack level language (only the higher level Solidity). Isn't it possible to write whatever language you like on top of that stack based language?

There is a proposal[1] to upgrade the current EVM to a WebAssembly based VM. Since webAssembly has a llvm backend, any language with a llvm compiler (which is most of them) could be used to write contract code.

1. https://github.com/ethereum/EIPs/issues/48

This is a vast oversimplification of the problem. LLVM is a compiler IR; nothing more. It is not portable (you cannot generate IR for one target and have it work for another target) and it does not trivially map to the semantics of most languages beyond C.

A programming language is a combination of many components; assembly optimization and target code generation is just one important part of a much larger picture.

I'm only responding critically because I've seen this trope that LLVM is some sort of universal programming language target way too often now. It misleads people into underestimating the scope of the actual problem. LLVM is not a panacea.

If you really want to make your platform programmable from any programming language, invest time into a well designed C API. Your users will thank you.

This is addressed in the linked issue.[1] Your criticism is the reason why (a subset of) WebAssembly is used, not LLVM IR.

1. https://github.com/ethereum/EIPs/issues/48#issuecomment-1690...

theres also the issue that committing to too low level an IR really makes it hard to do nice optimizations in a portable way! :'(

Should also point out that Juno can run EVM, via Masala, which is our stand-alone EVM interpreter. (https://github.com/slpopejoy/masala)

One thing EVM gets right is being a deterministic state machine -- giving rise to the possibility of "diffed" outputs, which is a feature of Hopper. This makes it amenable to offering a sidelong key-value store that is 100% verifiable, offering fast restarts and (dirty) reads.

Hopper's main goal is to reduce the surface area of computation, in order to focus on the problem of mass-conservation and transactionality. In EVM you have to code all of this stuff yourself. As we've seen, this requires a LOT of code.

EVM also bundles in a notion of accounts, which Juno does not.

Does this project actually escrow value, via PoW, or is it merely a message passing protocol?

the hopper language (the version used in this repo is an earlier snapshot of work from this fall that essentially a minimal scheme / lambda calculus with program level transactional memory) provides mechanisms for first class ownership. Current hopper master is under a huge amount of churn towards the full language we're building, so unless you enjoy reading compiler code bases under heavy active dev, the best i can say is this: stay tuned :)

linear logic provides a nice vehicle for modelling first class ownership. namely: holding a value in a program IS owning it. That plus a lot of ideas from languages/tools like Agda, Coq, Lean, and Idris along with some of what i've learned being an occasional contributor to GHC, plus general PL tech, are going into Hopper, though the current code base

Cool project!

Are you using dependent linear types? Or are you using dependent types some places, and non-dependent linear types for the ownership semantics?

Excellent Question. The notion of linearity were starting with for type system design corresponds with runtime linear usage, which Means linear computations that are pure can be lifted into types because they don't have any runtime usage.

One of the More surprising / interesting realizations we had recently was that the copattern matching for coinductive Data as seen in Agda is exactly what's needed to define pattern matching sanely on certain linear type operators like &

Which then let's you very succinctly model problems like having cake vs eating it. The original escrow of deliciousness vs the pretty cake

Will you be crowdfunding?

that not currently planned, thanks for asking! But once things are a little bit more mature (with the design a bit more visibly articulated, contributions / collaborations over at https://github.com/hopper-lang/hopper will be more than welcome :)

I'm hoping to end up with a very nice tool that I hope will be used in a surprising diversity of situations, but such discussions will be more intelligible once its not just a compiler ir core and runtime :)

Reply on news.ycombinator.com