5 ms·

Byzantine Fault Tolerant Raft With Smart Contracts

71 points by luu 11y ago

carterschonwald 11y 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 11y ago
  If one of the nodes goes rogue and tries to flood the network with noise, how does the system prevent denial of service?
  - carterschonwald 11y 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 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 https://github.com/uwplse/verdi is the associated coq development )
  - buckie 11y 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.
  - spopejoy 11y 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 11y ago
This is really neat. How does a system like Hopper compare to the Ethereum Virtual Machine?
- carterschonwald 11y 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 11y 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?
    - cdetrio 11y ago
      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 https://github.com/ethereum/EIPs/issues/48
      - adrianm 11y ago
brighton36 11y ago
Does this project actually escrow value, via PoW, or is it merely a message passing protocol?
- carterschonwald 11y 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
  - brighton36 11y ago
    Will you be crowdfunding?
    - carterschonwald 11y ago
      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 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 :)
  - thedatabase 11y 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?

71 points by luu 11y 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 11y ago
If one of the nodes goes rogue and tries to flood the network with noise, how does the system prevent denial of service?
- carterschonwald 11y 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 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 https://github.com/uwplse/verdi is the associated coq development )
- buckie 11y 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.
- spopejoy 11y 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 11y ago

This is really neat. How does a system like Hopper compare to the Ethereum Virtual Machine?

carterschonwald 11y 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 11y 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?
  - cdetrio 11y ago
    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 https://github.com/ethereum/EIPs/issues/48
    - adrianm 11y ago

brighton36 11y ago

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

carterschonwald 11y 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
- brighton36 11y ago
  Will you be crowdfunding?
  - carterschonwald 11y ago
    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 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 :)
- thedatabase 11y 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?