Byzantine Fault Tolerant Raft With Smart Contracts

by luu • 10 years ago

71 19 10 years ago

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 :)

drcode• 10 years ago

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

carterschonwald7• 10 years ago

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 )

buckie• 10 years ago

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.

spopejoy2• 10 years ago

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.

zmanian• 10 years ago

This is really neat.

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

carterschonwald7• 10 years ago

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 :)

aakilfernandes• 10 years ago

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?

spopejoy2• 10 years ago

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.

brighton362• 10 years ago

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

carterschonwald7• 10 years ago

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

brighton362• 10 years ago

Will you be crowdfunding?

thedatabase• 10 years ago

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?

Byzantine Fault Tolerant Raft With Smart Contracts

Related Stories