Darpa Contract Awarded to Verify Blockchain-Based Integrity Monitoring System(guardti.me)
guardti.me
Darpa Contract Awarded to Verify Blockchain-Based Integrity Monitoring System
http://guardti.me/2ciE3wp
8 comments
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.
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.
>> "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.
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.
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...
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.
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...
https://media.voog.com/0000/0036/0235/files/Black_Lantern_da...
The article mentioned that the project includes formal verification. From a moment scanning Galois' web page: https://galois.com/research-development/software-correctness...
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
https://en.wikipedia.org/wiki/Linked_timestamping
[deleted]
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.
Saving the next person the time. Links to both:
Copilot https://galois.com/project/copilot/
Cryptol https://en.wikipedia.org/wiki/Cryptol
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)
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?
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...
https://blog.ethereum.org/2015/08/07/on-public-and-private-b...
Yes.
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
edit: Updated question to be more clear of intention
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)
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'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.
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.
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
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
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
It's available from O'Reily: http://shop.oreilly.com/product/0636920032281.do
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?
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?
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...
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...
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...
NATO is also looking into blockchain uses: https://www.ncia.nato.int/NewsRoom/Pages/160425_Innovation.a...
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.
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.
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.
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."
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."
> 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.
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.
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.
[deleted]
Surely you agree that it's possible to prove x>0 is true after executing this program:
> 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.
if(x <= 0) {
x := 1;
}
> 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)
It's amazing that they seem to have built a $50 -$100 million dollar business here.