We know it’s part of our jobs to make these ideas understandable. That way more people can join the dialogue and think of ways this infrastructure can be used to build services for their communities, which may be really far from the nearest computer science program. So we decided to add a lighter approach in hopes of making it fun for people to learn.
But I'm hugely disappointed to see that they went with C and C++ for their new core codebase. This is the kind of code that needs strong safety, security, and correctness guarantees, and here in 2015 we have several mature languages with better safety & correctness guarantees.
C# and Java are both mature and mainstream, and either would have been a sane choice. Go is slightly less mature but also a safe and conservative choice.
(I personally love where Rust is going too, but I could excuse people for not choosing it yet due to immaturit.)
That said, I agree that C# and Java are good options.
Node and Mongo are moving hundreds of billions daily in HFS shops.
There is no magic but there are strong constraints that shift reliance for correctness from fallible human programmers and peripheral tools to the type system and compiler, providing better integrated, systematic assurance.
And Rust gives you fine-grained memory control without sacrificing safety -- unlike the others it has no garbage collector, and instead proves allocation safety at compile time. In Rust you can know for sure exactly where your key has been copied and when it will get deallocated (to the extent that any program running in virtual memory on normal hardware can know that).
Although I agree that these are the less mature choices, and it's reasonable to reject them for that reason.
It's certainly had a few issues, though I haven't looked closely enough to know which are due to the lack of memory safety, etc: https://en.bitcoin.it/wiki/Common_Vulnerabilities_and_Exposu...
Example: seL4 is written in C (as in, written by hand by fallible humans--not compiled down from a higher-level language ). But, the C is written in such a way that it is feasible to prove its equivalence to a Haskell prototype which had previously been proven correct.
Yes, language choice can be important. But, the degree of its importance depends on what you're building with it and how you're using it.
I think with a very modern C++ approach and very careful coding you can rock out. Yeah not everyone has this, but the losses from using Java is just so huge!
I've been to at least 200 software conferences in my life and never heard speakers like Linus, Ken Thomson, RMS, Gordon Letwin, DHH, Anders Hejlsberg mention "correctness guarantees".
I'm not talking about a whole-program correctness proof -- although those do exist too.
I can only read those lines so much before I get the feeling of being whitewashed. How does it work? Where is the data?
I'm reading the white paper now, but I felt compelled to post this comment after I read through yet another 10 paragraphs of exactly what I described above.
Something that takes on distributed consensus is a fantastically interesting project, this is so frustrating!!!
He is even credited in the changelog: http://lwn.net/Articles/131744/
::Sigh:: This sounds like it does not even speak to one of the major fundamental issues of their approach; which I pointed out in 2013 (https://bitcointalk.org/index.php?topic=144471.msg1548672#ms...) and appeared to play a critical role in Stellar's spontaneously faulting, and has been avoided in ripple by using effective centralized admission to the consensus in the system to ensure a uniform topology.
The (generalized) ripple "as-advertised"* consensus model can only be safe if the participants trust is sufficiently overlapping. In spite of requests by myself and several others (E.g. Andrew Miller) Ripple never formalized the topology requirement, much less how users are to go about achieving it. This paper goes forward in formalizing it, but still provides no guidance on achieving it; and absent that the only reliably way I know to achieve it is to have a central authority dictate trust. (*Ripple, as-deployed, centrally administers the "trust"; and Stellar faulted when it failed to do so and switched to a fully centralized approach (at least temporarily))
Consider a trivial example of two fully meshed subgraphs of 100 nodes each with an overlap of a single node. Assuming that each nodes behavior is tolerant to at least one ill behaved node, then both of the subgroups can come to a consensus (achieving at least 99 out of 100) about mutually exclusive state, and this can happen spontaneously without any attacker. More complicated partitioning-- ones involving many nodes in the min-cut, or more than two partitions-- are possible, to avoid it there must be 'sufficient' overlap.
Deciding on what the 'trust' topology must be to achieve safety requires non-local (and presumably private) information about what everyone else in the network trusts. The required minimum set of additional edges to make any particular natural trust topology into a safe one may have no relationship to whom anyone actually finds trustworthy in the real world. As far as I can tell no mechanism is proposed to establish a safe topology; just "the responsibility of each node".
To me that sounds a lot like saying "It is the responsibility of each node to not connect to any faulty nodes." Its a very strong assumption.
Separately, this system proposes a kind of consensus which is weaker with respect to blocking than e.g. Bitcoins. This is perhaps made most obvious by the point at the end about being unable to use the consensus to safely arbitrate global parameters (like system settings or version upgrades), something we do regularly in Bitcoin. It isn't clear to me why the authors believe that the system is fit for cryptocurrency use when it cannot guarantee eventual agreement about _all_ of the state. In Bitcoin the transaction 'light-cone' from coins splitting and merging appears to grow exponentially for most coins, so a failure to reach consensus on one transaction would eventually block most transactions. It's not clear to me if all participants could reliably detect stuck statuses and avoid dependance on them (if they could, why cant consensus continue). I'll need to read more carefully to understand this point.
A priori, we cannot definitively answer what kind of topology will emerge. But there is certainly precedent for building a robust network out of pairwise relationships, namely inter-domain routing on the Internet.
While inter-domain route agreements show precedent for building a robust network out of pairwise relationships, might this particular class of agreement also work because it happens to be a "small world" where failures are obvious? That is, the set of major AS operators is small enough that all the major players know one another (since ICANN) maintains a centralized list of who owns which AS number), and bogus route announcements are easy for an AS operator to detect since they coincides with floods of angry tech support calls asking why www.foo.com no longer loads (or loads www.bar.com instead). By contrast, it seems that Stellar is geared towards environments with neither of these properties--large worlds with hard-to-notice failure modes.
I ask because I'd love to hear your thoughts on how to select quorum slices when considering the political and economic incentives that might influence which node operators I choose to trust. Specifically, do you foresee the emergence of a small set of big-player node operators that application developers almost universally (and blindly) select for their programs' quorum sets, like how web browsers and OEMs regard CA operators today? How can Stellar help users do better than blindly trusting a small set of operators? I'm assuming that the fact that big-player node operators must nevertheless externalize the same slot values in order to enjoy liveliness makes it easy for the application to automatically detect any equivocation? If so, how would nodes be deployed to resist DDoS attacks that try to break the vast majority of usres' quorum sets? I'm getting the impression that there's a missing precondition here that for a large-scale Stellar deployment to be successful, there must be a very diverse set of quorum sets.
I can't predict the future, but I do think it is likely that a bunch of de facto important players will emerge and have fairly complete pairwise dependencies. One reason is that Stellar follows a gateway model, where counterparties issue credits. So for example, down the line people might want to store their money as Chase or Citibank USD credits. So people will already have some notion that some participants are trustworthy enough to hold their USD deposits, and these institutions will emerge as important. If I'm a Citibank customer and you send me money, I obviously won't consider the payment complete until Citibank says it is. And of course Citibank is likely to want to depend on a bunch of institutions they do business with, so even just one bank should give me good transitive reachability.
But the nice thing about safety is that you can reduce any individual party's trust by depending on more people. So for example Stellar will run a validator node for the foreseeable future, and their incentives are different from Citibank's. To gain more trust in the system, I might want to wait for both Stellar and Citibank to agree before considering any payment fully settled.
Now, regular nodes add the non profit node to each of their 2 member set slices. If one of the bigger guys colludes, the system is only blocked, because now the regular stellar users have depended on the non-profit node in each stellar slice, who has seen the collusion and isn't externalizing bogus transactions. Once the collusion is published by the whistle blower node, regular stellar nodes can remove those slices that contained the bad node, and the system moves forward.
Now this is a completely contrived example but you can generalize it as a chain of trust webs, where i listen to the someone, someone listens to me and the person i listen to, and so on.
The person who is being attacked cares, right? Is there a way for a Stellar node to realize that it has been partitioned from the real network?
There's one sense in which FBA is stronger than the Internet analogy, however, it that is is actually testing transitive reachability. So instead of just making sure you can talk to those 50 web sites, you actually make sure all of those 50 web sites can talk to all the sites they consider important, and so on, until you get the transitive closure, which is basically the notion of an FBA quorum.
This requires you to trust the 50, correct?
Ah. What mechanism assures this consistency of this information?
> at one node might or might not be a problem
How could it not be a problem? If that is the totality of the network, and the network is 1-fault tolerant, what prevents spontaneous divergence of the state?
> most likely cause of such a topology is a Sybil attack
"likely"? It's not clear what you mean there. What statistical model have you adopted that allows you to reason about the likelihood of various topologies?
Social networks usually appear to have small word behavior where its usually very easy to draw lines that describe disjoint local-majorities (or fairly large local-super-majorities).
I agree that a sybil sticking on a bunch on a bunch of extra 'nodes' and the sybil nodes diverging as a result isn't interesting case. What I do think is interesting is what mechanism will prevent user's honestly stated trust (much less politically manipulated trust) being a bad topology?
What is the procedure that I can follow, that if everyone else follows it, results in the correct global behavior (with high probability)? What are the additional assumptions required to achieve that and make it secure? Why are they plausible? Do they provide decentralization? (I can suggest on procedure which works: Stellar tells everyone who to trust; but it completely fails at decentralization so I assume that isn't the goal.)
In Bitcoin our security assumption is that the computational majority of participants conform to the protocol ('are honest') and these participants are not completely partitioned from each other. People can then think about-- or debate-- how reasonable those assumptions are.
(There are alternative formulations of Bitcoin's security which also argue about how plausible these assumptions are given economic incentive assumptions; but even this most simple set of assumptions gives people something easy to reason about.)
Can you give a parallel (informally stated, but equally comprehensive) version of the security assumptions for your consensus system?
> But there is certainly precedent for building a robust network out of pairwise relationships, namely inter-domain routing on the Internet.
The Internet is _wildly_ inconsistent. Asymmetric routing is the norm, the internet frequently suffers small partitioning and loops; single malicious parties at the edge can frequently inject bad state that is accepted globally, congestion and blocking happens multiple hops away from users where they have no recourse. The internet is not a consensus system, and these issues are not usually hugely problematic; someones brokenness doesn't involve your traffic generally effect you, you can route around problems locally. Ephemeral routing and ledgers are fairly different problems. Ambiguity about the ownership of a coin eventually effects almost everyone. I'm not seeing the connection you're making there.
I certainly agree that useful systems can be built from pairwise relationships: The original ripple design for pure IOUs without creating its own cryptocurrency prior to opencoin buying the ripple name was such a system, it had no need for a global consensus (except perhaps in certain atomic unwind cases)-- only the participants in a particular IOu transfer needed to be involved. It is not at all clear to me that a safe global consensus system can be built from pairwise trust.
Part of the goal of SCP is to leave such policy questions up to the market and see what kind of architecture emerges. Our hope is that this flexibility combined with the lower barrier to entry will lead to greater financial inclusion as people build on our platform. But if we add too many policy restrictions, we risk heading off unanticipated innovations. (Heck, someone might literally replicate the Bitcoin policy and configure their quorum slices to trust 67% of whoever mined a Bitcoin block in the past week. That wouldn't really make sense, but it's possible.)
That said, what you're getting at is that with flexibility comes risk. We can't a priori rule out the possibility that organizations will choose bad quorum slices that violate safety. But we need to ask under what circumstances people care about safety and why. People obviously won't care about forks if one of the branches is purely a Sybil attack. But they likely will care if "real organizations" diverge, for some notion of that term. The reason, again, is that at some point the "real organizations" will affect one another in the network, however indirectly--maybe after a chain of five payments. That kind of indirect link is precisely what FBA quorums capture in the transitive closure of slices. So if everyone depends on the financial institutions they expect to do business with, and the whole economy is in fact interconnected, then Stellar will be safe.
I obviously believe such interdependence exists, and fully expect Stellar to be safe, but I can't predict exactly what the network will look like. Nor do I want to, as this could limit innovation. Only time will tell how this plays out.
Indeed, the security model provided by Bitcoin consensus system may not be fit for any particular purpose. But it has one, and so we can think about it and decide what purposes it may or may not be fit for, and think about under what conditions it will be safe or not safe.
> is to leave such policy questions up to the market and see what kind of architecture emerges
Users of a system take actions. In your system, it seems, the collective actions of all the users result in an effective security model. You refer to this as leaving it up to the market.
The resulting security model--the conditions of success or failure, the invariants which must hold--may be unknown to any of its participants; it may be even unknowable to any one human mind. It may, and almost certainly will, change over time. A user adopts the system today, but finds tomorrow that it is behaving in a way which was previously impossible, including restrictions being sprung on them later--the possibility of which is a kind of restriction in and of itself.
> Heck, someone might literally replicate the Bitcoin policy and configure their quorum slices to trust 67% of whoever mined a Bitcoin block in the past week.
Even your best outcomes with pinning the state to "real organizations" leave me wanting to cite Jo Freeman's "The Tyranny of Structurelessness" as a source for concerns--but I can't, because by failing to state a specific security model, you have a fully general defense against any attack or failure mode: "okay, don't take that risk, the invisible pink hand can choose another set of tradeoffs instead". As you've helpfully demonstrated above (by claiming to generalize the Bitcoin consensus model), there is no conceivable attack for which you couldn't say the system addresses it, as the security is basically external. In some sense you might as well have just shipped a C compiler, pointed out that it was fully general for whatever the market might choose to do (good or bad), and said it was up to the market.
[As an aside, Bitcoin mining is not just creating identities via hashcash; Blocks commit to the past ledger state-- it's effectively a signature itself--, and this is integral to the security model; without that those identities could concurrently create unbounded conflicting states with constant energy usage. See, https://download.wpsoftware.net/bitcoin/pos.pdf for a more complete discussion of the subtle details around that.]
For a market to choose, there must be a choice and there must be intent and understanding. Participants need to be able to trust that their choices are effective and won't be completely undermined by the choices of others, or at least understand how their choices might be undermined and be confident enough that such an outcome is unlikely. For the market to choose, people would need to understand the global ramifications of their actions and the actions of others, but you've seemingly provided no tools to reason about these.
I'm not complaining that there is risk--there is that aplenty, and in Bitcoin too for sure--but that there is no commitment to a sufficiently complete concrete security model at all, which makes the risk impossible to assess. Bitcoin users will also sometime make arguments about the suicide pact of the interconnected economy, but they do that as an answer to what if the first plausible mechanism fails. It probably okay that a system has generality and can potentially fullly accommodate the whim of man, but the more our systems rest on that the more opaque they are in practice.
I really think Stellar should develop and transparently state specific technical 'plan' on how the system should be used-- how trust should be configured globally-- and defend the plausibility and desirability of that model, describe who will and won't have the power to control the system as a result, how centralized it will be, how people can choose to configure their own systems to bring about that outcome, and how we can tell if it has achieved a configuration which can deliver on that plan (preferably before observing a failure). Maybe even multiple such plans, if it were possible to analyze their interactions.
Without that, I can't shake the impression that what you're actually saying isn't 'leave it up to the market' but that instead what you're actually saying is 'leave it up to chance'.
That said, my _prediction_ is that it will work fine mostly, occasionally there will be concerns about people splitting off into islands, and a resulting second-order consequence is that people will start putting the Stellar equivalent of blockchain.info onto their trust list in order to ensure connectivity to the "main graph" (I had actually cited The Tyranny of Structurelessness in my own responses already :) ), and this will just have to be the social-network-consensus version of the GHash.io scare and we'll be fighting against people's private interests to be lazy to reduce the risk of that happening.
Because the prior version _already_ faulted in production as a result of having a trust graph that didn't meet the prior criteria needed for safety. The prior version also resulted in centralization in practice (in it's ripple instantiation; kind of neat that the ripple->str-reboot let us see both of the predicted failure modes play out, even though they were largely mutually exclusive)
The latest work is intended to relax the requirements/consequences but still provides no guidance or tools for achieving the required topology in practice.
By all means, clearly label these efforts that have have taking a "you haven't yet proved its broken" approach to safety/security; and I won't complain about them. Absent that, I just normally expect that when someone produces a cryptographic product that they've actually given some care to their security.
> consequence is that people will start putting the Stellar equivalent of blockchain.info onto their trust list in order
Then if they're anything like the Bitcoin world's blockchain.info-- which is regularly in a confused state--, I'm may soon find myself the proud owner of infinity STR, I guess? ( Screenshot someone else sent me of the actual BC.i site one day a while back: http://people.xiph.org/~greg/21mbtc.png )
"testing is making sure it does what it should, security auditing is making sure that is all it does"
In SCP the topology is public and conveyed with each consensus packet. So people will be able to tell when the graph is vulnerable.
Improving the definition of topology requirements for correct consensus is, far from being 'ignored', exactly what Mazieres has been working on all this time. And as you admit, those requirements have now been formalized and the information to check them is conveyed in the consensus packets; they are just not trivial to check by hand, and we have not yet implemented a check for them in stellar-core (this will be forthcoming, see roadmap).
I'm also interested in how the explicit quorum slice data for each node can be used to maintain quorum intersection over the entire network as new nodes join.
The collective actions of all participants result in an effective price model, the causes of which are unknown to any of its participants and likely unknowable to any one human mind, and which changes over time in ways that are highly opaque.
In the market at large, participants certainly don't need to understand the global ramifications of their actions, only the local ones. I don't see why that isn't the case here as well.
(For what it's worth I want to point out that like Walter, I really enjoyed reading this discussion, even if much of it is over my head.)
The primary reason why that does not apply here is because nobody is selling "the market at large" to you as a cryptographically-secure decentralized consensus system. And besides, those ledgers are edited all the time by Authorities; it's irrelevant to this topic.
Edit: you are attempting to reason by analogy about a pricing system, and then trying to apply it to proof-of-work consensus? May I ask why?
Edit in response to your edit: It just occurred to me that most of the critiques that nullc was making were in very direct correspondence to critiques one could make of the price system. I have no idea if this analogy is useful, but it seemed awfully coincidental.
But they're not keeping consensus ledgers for limited supply cryptocurrencies. Any of these failures or faults can allow a coin to be spent twice (or other mutually excluded transaction) with parties that have different views of the system, the result-- and any transaction which is casually depended on the conflict-- can never be part of a common system.
So it's like someone manipulates the market economy to convince you to buy a cheeseburger most other parties think they sold to someone else, and now your hand cannot interact with your neighbor's door because your hand contains atoms that-- as far as your neighbor's door is concerned-- aren't part of your hand but are instead part of my foot.
Markets are a tool. They have their applications and limitations, building the security of a cryptocurrency in an adversarial environment out of them sounds like a plan for failure. No less than using a cryptosystem in a place where you really needed a market may not give great results.
But you don't have to take my word for it, the prior consensus model in Stellar _already_ faulted, all on its own when, the requirement for the trust topology was violated. This fault wasn't a surprise, I (and others) called it out years before-- but the vulnerability of the system was publicly ignored by Stellar's creators while they ran Ripple and Stellar's advisers (including Mazieres, who was an adviser listed on the Stellar site on day one) even as they facilitated the sale of their ripple-reboot asset to the general public. It was not acknowledged until it knocked their system out. The improved consensus may better confines the failure domain, but retains the property that the safety of the consensus is largely external and depends on particular topological constraints without a procedure that provides any assurance the constraints are likely to be met.
Another response to me argues that it will probably be fine; but this flys in the face of reason. The same property existed before and it demonstratively wasn't fine.
If you look at the old BCT thread, I was a big fan of the original ripple IOU system, before ripple labs bought the name, and had recommended it as a potentially fruitful area to many people. The original system could potentially have been implemented without any global consensus at all, which was a large part of why I found it interesting-- Global consensus is enormously costly. But functionality like a new cryptocurrency currency for the purpose of funding the company and the integrated non-interactive rippling (which apparently has been largely turned off in ripple now due to other security vulnerabilities) brought back in the global consensus requirement. (The result was that I felt I had to go edit all my old posts to remove my recommendations, since the system was wildly changed to be something else)
(Bit sleep-deprived right now but) FWIW, here's my take: Bitcoin tries to be too many things to too many people. Original ripple was a great response, though without providing a strong solution to the topology problem (manual processes for trust agility).
Now, both fail to "do one thing and do it well". Fundamentally, the functions 'settlement protocol', 'currency' and 'client program' (ie. implementation of protocol) should be well delimited. Besides these, Bitcoin now effectively attempts to do more (expensive paid public sequential datastore and agent-based computing platform, ill-conceived invoicing system, future revenue-guarantees for early adopters/special nodes, etc.)
This brings me to some points I feel have not been considered in this thread: (1) People don't put absolute trust in a settlement network or currency. The de-facto means of managing risk is to simply to limit exposure: either by sending smaller amounts sequentially over time and validating delivery with your endpoint (out of band) prior to sending the next 'chunk'; or by splitting a transaction across multiple currencies/settlement networks/(anonymous/temporary/unpredictable) points of network connectivity. (2) No system fits all people. It's great that the stellar notion addresses one of Bitcoin's most glaring issues: latency for real time / retail transactions. However, it does not necessarily meet all of Bitcoin's capabilities, nor should it aim to. A real world user should have a computationally available means of comparing these networks against real time requirements to select an appropriate path (in terms of risk mitigation strategy, temporal requirements, maximum transaction size limitations, secrecy requirements, and any other execution and routing goals/preferences). (3/corollary) The key issue in present-era financial systems may be that business logic around the true properties of a financial transaction, network or settlement partner are very rarely formally defined (ie. typically many pages of indecipherable legalese that amount to 'we promise nothing and have well paid lawyers', with no computationally usable community metric for SLA enforcement on latency, reliability, instances of failure, etc.)
My thoughts here have remained fairly constant for the last four years: what is really needed is a business-level transaction protocol that disclaims any affinity at all for (a) the currency or currencies in a transaction; (b) the settlement systems used; (c) the endpoint identification system used; (d) allows the discussion/agreement of a realistic range of resolution strategies for common problems in business-level transactions; and (e) facilitates flexible (indeed, multi-path) routing between endpoints across arbitrary financial service providers, potentially using multi-hop/multi-asset pathways shortlisted in real-time through actor and transaction-specific requirements.
A valid settlement path should be 'buy expensive art, get on a plane, deliver to mansion'. Likewise, a valid settlement path should be 'plant a tree and share the GPS location and have it manually validated by a third party'. (These are outlying examples, but an example of the degree of flexibility that should be aimed for in the long tail of latency and use cases. The shorter side is obvious: redundant multi-provider fiscal routing (even across conventional banks), level playing field for emergent financial systems and the conventional ones, etc.)
Some time ago I tried to make proposals in this area at http://ifex-project.org/ (IIBAN perhaps most successfully) but have not been able to dedicate much time to the notion lately. I do however feel it is relevant and am willing to jump at any time to work with others to move the notion forward. If you two are interested I'd love to get together and bash something formal and extensible out of this line of thinking. Tentative proposal: meeting in Europe next month?
Failing to ensure quorum intersection in my quorum slices choice will have local repercussion and may befoul nodes that depend on me but does not prevent global functioning if the rest of the topology has quorum intersection.
I think your argument here is sane, but I also believe that under reasonable circumstance we can expect the Stellar network to be well structured. Yes some edge nodes may get befouled as you would in real life if you would trust an untrustworthy bank or health insurance.
Basically, any two UNLs must have 20% overlap to avoid any risk of a fork.
Any pointers for someone looking to gain an amateur understanding of this, or is this a topic of sufficient complexity that it precludes an amateur understanding?
Sybil attacks are not really directly applicable here since each node in the system picks its own quorum slices (basically the set of nodes that it trusts). There is no notion of global reputation and nodes do not need to know every other nodes to participate. Looking at the definition of quorum intersection section 4.1 should give you a sense of the conditions that are required on the choice of quorum slices for the network to function properly (quorum intersection ensures safety)
The proof exposed in the paper guarantees safety and liveness for the network provided a certain number of reasonable conditions are held true. What that means is that an attacker cannot force on intact nodes (definition p14) invalid transactions nor prevent the network from making progress.
That being said, (at least in the version I reviewed) there is no guarantee provided with respect to ensuring that all valid transaction will eventually make it into the network. Indeed a set of highly trusted nodes (present in a lot of quorum slices) could attempt to preempt a specific set of transactions X (originated by edge nodes) by opportunistically broadcasting valid transaction set V_i for each successive ledger entry i that explicitly do not include the targeted set of transactions X. Under raw SCP as described in the paper and for certain topologies this preemption could be real and this is the closest I can think of a Sybil attack. It's important to note that we still have liveness and safety in that case.
I believe the same kind of attacks to be plausible with the Bitcoin network and I know protection mechanisms against it are currently being evaluated by David, Jed and the rest of the team. I will let them share their progress when they think it's right. I also hope they will correct me if I stated anything inaccurate here!
This isn't anyone elses understanding. Can you suggest a mechanism by which it would be possible for a minority conspiracy to perpetually exclude a transaction in Bitcoin?
Whats the similar statement for 'trust' which is sufficient for security? Obviously "attacker is partitioned from the network" is sufficient, but not very plausable. I'm sure there is a better statement possible, but its not clear to me what it is.
Now let's look at the Stellar model in this same situation. We've got a bunch of large company nodes that are probably Gateways (for the sake of argument say JCB, Wells Fargo, Barclays, and Bank of Brazil). We've got a ton of other nodes that belong to research universities, and then we have a bunch of "non-profit" or hobbyist or whistle blower nodes. There's a nice graph topology between all of these. Then one day China comes along and decides its had enough. How does it attack the network in this case? By hacking enough organizations to take control of their nodes? Seems a bit more unlikely than it gaining 51% of hashing power on the Bitcoin network...
That's the Maginot Line attack, at Tim Swanson calls it. The more realistic attack is that China just hacks into five data centers and serves a warrant to another ten. An interesting property of the PoW incentive structure is that there is actually fairly little incentive to protect oneself against hacks, so I would not be surprised if it was fairly easy.
> By hacking enough organizations to take control of their nodes?
The key point in Stellar consensus is that even if enough nodes are hacked, then users can just stop trusting them and switch to other nodes, and so the network would "route around" the damage. With Bitcoin PoW, there's no way to exclude an attacker from participating; you have to accept their work just as much as everyone else's.
As for eclipse, the model is so fundamentally different that it's not clear that there is a direct analogy for those network attacks. What do you have in mind? I'm not saying that it's obviously safe, just that attacks on the network protocol would have a very different flavor.
i.e. FBA relies on a web of trust, not just on showing up and churning out hashes or whatever.
To me, though, it would be more interesting to prove the implementation correct. Rather than trying to prove an existing C++ implementation correct, it's probably more feasible to reimplement the algorithm within Coq and extract to runnable code. Verdi already supports that, but unfortunately it doesn't support disk state.
In addition to using gateways, as diyang suggests, there is another way, but you first need two things
1) Someone on the network who you trust. This may be your bank, but it could also be something else. I'm not going to tell you who or what you should trust, and to what extent, that is a decision that should be always in your hands
2) A path between the entity you trust and an entity that either you or your bank has access to.
Until #2 exists, you can do what the poster below just said: use a gateway. This is not recommended, as they are probably going to track you and it may not be always possible to deal with them in a humane way.
So really it depends on what your bank is, whether it makes sense to draw money from your bank into another form/service that is compatible with a service that stellar can talk to. What bank? What country? These things are going to matter on the global scale.
This post is about keeping everybody's copy of the ledger the same using a process called consensus. Even if there were no gateways, there still is the problem of ledger agreement, so we'd still need consensus. Gateways and consensus are orthogonal. You can learn more about consensus here: https://www.stellar.org/learn/explainers/#Consensus
You should look in the white paper to the definition of an FBAS which differs from epaxos (while epaxos is egalitarian, SCP is federated). All related proofs are included in the whitepaper, the central one being theorem 3 in 4.2. Finally the protocol specification (Figure 15, p28) is also very interesting.