Darpa Contract Awarded to Verify Blockchain-Based Integrity Monitoring System | Hacker News Reader

Darpa Contract Awarded to Verify Blockchain-Based Integrity Monitoring System

guardti.me

120 pointsm54555 comments

Guardtime is set of tooling around a FIPS 140 timestamping appliance. Systems on the network submit hashes of their logs to the time stamping. Assuming the appliance remains secure, you can go back in the event of compromise and prove that your logs are unaltered up to a certain point.

It's amazing that they seem to have built a $50 -$100 million dollar business here.

>> "Assuming the appliance remains secure"

Makes me wonder what mathematics would prove this, or if it's assumed to be out of scope, and if so, what else is out of scope too.

The article mentioned that the project includes formal verification. From a moment scanning Galois' web page: https://galois.com/research-development/software-correctness...

I'm pretty sure the Guardtime product is a Merkle tree of timestamps. I'm also pretty sure whatever protocol they use to maintain it would _not_ be immediately recognized as a "blockchain" protocol. Of course the protocol can be modeled and checked. The question is why does anyone think that this activity can apply to "blockchains" in general. But, welcome to the world of industrial research funding.

(I work for Guardtime; I’m happy to answer any questions.) Some online resources might not make it very clear, but the KSI blockchain is indeed a blockchain; for example, new blocks are released periodically (1 block per second on average), and the new blocks contain hashes of the previous blocks, among other things. Then, blocks get distributed around so that users can verify their data against these blocks, etc.

Most people associate "blockchains" with a protocol by which the "blocks" are inserted. Usually these things revolve around proof-of-work, proof-of-stake, proof-of-space, fairness criteria, etc. I think everyone gets that the Guardtime product is hashtree. From a formal verification perspective, the critical behavior is probably in the protocol, and most likely not the implementation of the datastructure or database.

One way to look at it is that KSI is a proof of stake blockchain where the stakeholders are (mostly) fixed. Often people would call that a private blockchain (or a consortium blockchain), to use the terminology from the following article:

https://blog.ethereum.org/2015/08/07/on-public-and-private-b...

Thanks for that clarification! It is a great pleasure to talk with an knowledgeable person like you.

> 1 block per second on average

What stops a double-spend or other attacks like that in a 1-second timeframe? The 10 minute threshold of Bitcoin was chosen under belief that the network would be settled after roughly 10 minutes.

The speed comes from the fact that private and consortium blockchains tend not use Proof of Work (at least not as the only algorithm; you could mix and match, if you wanted to). Instead, such blockchains tend to use voting-based protocols (e.g. Proof of Stake), where a certain subset of nodes are trusted with voting rights, who together vote to approve the next block. In some systems you also have automatic punishments built in to incentivise correct behaviour (i.e., if someone attempts to fork a blockchain --- for example by voting for 2 conflicting forks -- and if other nodes see any evidence of that, the node who attempted the fork could automatically lose their rights as a trusted validator, and may also automatically lose a lot of money or face legal fees.)

I'm from Guardtime - this is our secure appliance that we built with a team of engineers coming out of the US Military Ant-Tamper community: http://bit.ly/2cgXiDu

Redirected link from bitly link above:

https://media.voog.com/0000/0036/0235/files/Black_Lantern_da...

What's wrong with posting a bitly link?

Transparency

I was just reading the Wikipedia page on Linked timestamping yesterday. Though I don't know that this is what Galois & Guardtime are doing.

https://en.wikipedia.org/wiki/Linked_timestamping

Well, when your adversaries are the likes of China, Russia, multibillion dollar corporations, powerful domestic adversaries, etc... you'd want to be absolutely certain your safeguards are as strong as possible.

RSA key fobs were an extremely simple invention, yet they are ubiquitous in enterprise. Often the value of a product lies not in its technical sophistication, but in whether that product solves an unmet business need. Spotting these opportunities is the difficult part. That is where these entrepreneurs add value.

It's cool that Galois got this contract. They're a very nice Haskell shop out of Seattle responsible for projects like Copilot and Cryptol.

Out of Portland, actually.

Yep, sorry about that!

Saving the next person the time. Links to both:

Copilot https://galois.com/project/copilot/

Cryptol https://en.wikipedia.org/wiki/Cryptol

As far as I can tell from the article, they are using the same kind of technology which prevents people from falsifying their account balance on Bitcoin to prevent intruders from covering their tracks in a secure computer system.

Specifically, it's a Merkle tree. From what I can tell they're not using anything else relating to "blockchains".

The signature for your data that has been signed is a chain of hashes which is used to calculate back to the merkle root.

Wikipedia defintion of blockchain[1]

> A blockchain consists of blocks that hold batches of valid transactions. Each block includes the hash of the prior block in the blockchain, linking the two. The linked blocks form a chain

[1] https://en.wikipedia.org/wiki/Blockchain_(database)

The very next paragraph describes blockchain databases as peer-to-peer protocols with some form of scoring algorithm to decide which blocks are part of the chain.

This has now been answered by someone from the team

I worked as a contractor for guardtime, and they're a great company, it looks like they are continuing to do great work in this area.

For those who are interested in an underpinnings of KSI: https://eprint.iacr.org/2014/321.pdf

They keep using the word 'block chain'. Is that the same idea as the bitcoin blockchain?

Yes.

No. The point of the Bitcoin blockchain is to provide ordering of transactions without a centralized timestamping service. This is a centralized timestamping service.

(I work for Guardtime.) KSI verification is meant to be decentralised; that is, no single (centralised) entity should have the ability to, for example, create fake timestamps. You can deploy KSI in various ways, so there can be, for example, one entity who controls access to the blockchain (but for example they still cannot fake any evidence).

Right, it appears you can have multiple physical tamper-protected boxes that agree with each other, which makes it federated, but not decentralized.

I tend to subscribe to the definitions laid out in the following article:

https://blog.ethereum.org/2015/08/07/on-public-and-private-b...

With something as important as blockchain verification, you would think DARPA would stop investing in private intellectual property.

Why is blockchain 'important' to Darpa? Because you are rooting for bitcoin or for some other non-specific to you reason?

edit: Updated question to be more clear of intention

Because it's a cryptographic proof. If their implementation is faulty they are vulnerable. It's very difficult to do correctly and many bugs have been found in bitcoin and other blockchain technology. This is pretty much one of the harder areas of computer security...

The blockchain is critical current & future technology, it's future is independent of Bitcoin's future.

Bitcoin is the first implementation of a blockchain system, but it's a technology, not Bitcoin.

All major log systems will be based on it; governments, banks, military, voting systems, etc.

Highly suggest reading the Wikipedia entry on Blockchain to learn more and think about how you might use it too: https://en.m.wikipedia.org/wiki/Blockchain_(database)

I am versed on the blockchain. My question was not regarding its merits or usages. My question was on your phrasing of importance and how blockchain would be considered important to Darpa.

Do they have publicly known projects where they intend to use it? The funding itself shows they find it valuable or at least are curious enough to spend but for what reason?

I'm a blockchain blockhead. Any more suggested reading?

Really basic like a) how will my debit card debit my money buying DD coffee?

If I create another book can I "get blockchain" (so to speak) to protect my work? Thus, I will need to make the right choice to be covered under a blockchain or not?

At 50000 ft I get the significance I think. I just cant even come close to explaining it.

I recommend "Mastering Bitcoin" by Andreas M. Antonopoulos. It provides great detail on how the Bitcoin network actually works, including the cryptography you need. Work through that and you'll know how blockchain payments work and have a good idea of how the technology can be applied to other areas.

It's available from O'Reily: http://shop.oreilly.com/product/0636920032281.do

Think of a blockchain like linked lists. The linked lists exist on the network and is peer to peer, so there is no central server that stores the data.

Whenever a new transaction is made, in the case of Bitcoin, a new node is created and joined to the linked list.

The bitcoin blockchain is limited in the sense that you can only buy / sell bitcoin. Ethereum is another up and coming blockchain that allows you to write smart contracts (contracts that enforce themselves). There is a whole community of developers working on developing decentralized applications for Ethereum blockchain now.

Come join us over at /r/ethereum

There are reasons that this an interesting technology other than simply rooting bitcoin.

For example, consider the challenge of monitoring strategic weapon treaties or nuclear proliferation agreements. Agencies can leave monitoring video cameras at locations and would like to insure that there is no way for one party to modify the captured data.

It doesn't work that way. The hashes can simply indicate proof of tampering, so instead you get (some) assurance that there was no tampering in the evidence.

Attackers can still modify the data. For example, if they modify the feed before the hash of the feed is introduced into the blockchain.

Edit; Security at that level is extremely difficult as their adversaries are much more powerful and well funded. I can understand in that respect why DARPA would want to invest a large amount into that area.

Because time is baked into the process, and there are alternate means of establishing the time of events that relate to treaty verification, actually it would work this way, at least with respect to a hypothetical video feed. I have intimate knowledge of treaty verification procedures and methods, and worked in collections relating to these activities for the intelligence community. The fact is that there is no video feed, and it's utility is of dubious value anyway, but in principle, a video feed could be secured this way.

It just seems like you're expressing contest of granularity. A simple example is a feedback loop that would still have the process be deterred by some time from collecting evidence, and from being detected. The process just prevents to a certain degree the tampering of evidence once collected.

They want to make a decentralized chat app based on blockchain tech among other things.

https://www.bloomberg.com/news/articles/2016-04-25/u-s-wants...

Yes, that was an odd DARPA RFP though, since amoung other paradoxical that RFP wanted to be able to delete parts of the blockchain after the fact.

NATO is also looking into blockchain uses: https://www.ncia.nato.int/NewsRoom/Pages/160425_Innovation.a...

Quote: "Galois is a leader in formal verification, a technique that goes beyond testing and evaluation to provide mathematical assurances that a system works only as intended in all cases."

Wait -- mathematical assurances that a system works only as intended in all cases? That's not possible. It pretends that the Turing Halting problem[1] is soluble.

Not that this claim is at all uncommon. I regularly see similar claims about software validation, by people who either do not know, or who don't want to acknowledge, that this problem cannot be solved in the general case.

1. https://en.wikipedia.org/wiki/Halting_problem : "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist."

Real computers are finite state machines, not Turing machines.

Correct but not relevant. No formal verification technique takes advantage of the fact that the computer has "only" 8 GB or RAM and 1 TB of disk space as its tape (~ 2^2^43 states).

You are correct that creating a program that verifies any other program is mathematically impossible. However, given some critical assumptions regarding the scope of the problem, we can use formal verification techniques to generate proofs for some programs. People in formal verification (https://en.m.wikipedia.org/wiki/Formal_verification) do research to find better ways of creating proofs for programs automatically.

Surely you agree that it's possible to prove x>0 is true after executing this program:

    if(x <= 0) {
        x := 1; 
    }

People have come up with techniques for reasoning about loops and recursion. Not in general, of course, but for some specific property (e.g., x > 0) and some specific loop (e.g., while(x <= 0) x := x + 1) there are techniques for proving that the property holds after the loop.

> I regularly see similar claims about software validation

Validation and verification are very different things. Verification is "my program meets these formal specs". Validation is "my specs accurately encodes the whole problem". Indeed, there's no way to do validation in a provably correct way. (But, of course, mathematics and statistics can help :-) ). The good news is that a lot of security and other bugs arise even once you have the correct spec. So verification can be useful even if it's impossible to perfectly validate.

> by people who either do not know, or who don't want to acknowledge, that this problem cannot be solved in the general case.

It's somehow ironic that you invoke the Talking problem since Turing himself -- AFTER having proven the Halting problem -- basically conjectured the creation of formal methods.

This formal verification walkthrough goes through the hows and whys of a recent project with Amazon that may have some answers for you. Obviously a different project but the fundamentals are similar https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/ (I work at Galois)

> that this problem cannot be solved in the general case.

They are not solving it for the general case. They are solving it for many specific cases. Presented with a system, there is no guarantee that this will be possible - there can't be, that's what the Halting Problem says. But there is also no guarantee that it will be impossible for the particular system under consideration - that is not what the Halting Problem says.

Reply on news.ycombinator.com