The MSR Ironclad project builds provably secure and reliable systems.
Home Page: http://research.microsoft.com/en-us/projects/ironclad/
License: Other
![microsoft-github-policy-service[bot] avatar](https://avatars.githubusercontent.com/in/95686?v=4 "microsoft-github-policy-service[bot]")
Could someone point to where the actual implementation source code of the (verified) distributed key value store lives? i.e. code that could be compiled into an .exe directly by a c-sharp compiler.
This repository is currently missing a LICENSE file.
A license helps users understand how to use your project in a compliant manner. You can find the standard MIT license Microsoft uses at: https://github.com/microsoft/repo-templates/blob/main/shared/LICENSE.
If you would like to learn more about open source licenses, please visit the document at https://aka.ms/license (Microsoft-internal guidance).
We have noticed that Ironfleet’s high-level spec [1] fails to ensure linearizability because it does not enforce exactly-once semantic. The seqno field of the request is used only to pair requests with replies but does not prevent a duplicate request (i.e. a request with the same client sequential number) to be executed twice.
Even though there is code both at the implementation layer and at the protocol layer that tries to ensure the exactly-once semantic, this functionality is not guaranteed to be correct through verification of the high-level spec, as one would expect.
To confirm this, we were able to modify Ironfleet’s code in such a way that it does not detect duplicate requests but still passes all the verification checks associated with Ironfleet’s high-level spec. This modification involved only changing a few lines of code that were associated with the highest_seqno_requested_by_client_this_view field.
An incorrect replicated state-machine implementation, with regard to this functionality, could cause serious problems to the application running above it. This would be the case even for a simple application like a counter.
Here is an example of a patch that passes the verification checks but allows the servers to accept duplicate requests:
diff --git a/ironfleet/src/Dafny/Distributed/Impl/RSL/ExecutorModel.i.dfy b/ironfleet/src/Dafny/Distributed/Impl/RSL/ExecutorModel.i.dfy
index 605b64d..86f38df 100755
--- a/ironfleet/src/Dafny/Distributed/Impl/RSL/ExecutorModel.i.dfy
+++ b/ironfleet/src/Dafny/Distributed/Impl/RSL/ExecutorModel.i.dfy
@@ -132,7 +132,7 @@ method {:timeLimitMultiplier 2} HandleRequestBatchImpl(state:CAppState, batch:CR
repliesArr[i] := newReply;^M
states := states + [new_state];^M
final_state := new_state;^M
- newReplyCache := UpdateReplyCache(newReplyCache, reply_cache_mutable, batch[i].client, newReply, reply, i, batch, replies);^M
+ //newReplyCache := UpdateReplyCache(newReplyCache, reply_cache_mutable, batch[i].client, newReply, reply, i, batch, replies);^M
i := i + 1;^M
^M
// Prove AbstractifyCAppStateToAppState(states[i-1]) == g_states[i-1]^M
diff --git a/ironfleet/src/Dafny/Distributed/Impl/RSL/ProposerModel.i.dfy b/ironfleet/src/Dafny/Distributed/Impl/RSL/ProposerModel.i.dfy
index 82835eb..4d86c1f 100755
--- a/ironfleet/src/Dafny/Distributed/Impl/RSL/ProposerModel.i.dfy
+++ b/ironfleet/src/Dafny/Distributed/Impl/RSL/ProposerModel.i.dfy
@@ -122,16 +122,16 @@ method {:timeLimitMultiplier 2} ProposerProcessRequest(proposer:ProposerState, p
^M
//var lookup_start_time := Time.GetDebugTimeTicks();^M
if proposer.current_state != 0 && ^M
- (packet.src !in proposer.highest_seqno_requested_by_client_this_view ||^M
+ (true || packet.src !in proposer.highest_seqno_requested_by_client_this_view ||^M
packet.msg.seqno > proposer.highest_seqno_requested_by_client_this_view[packet.src]) {^M
// var lookup_end_time := Time.GetDebugTimeTicks();^M
// RecordTimingSeq("ProposerProcessRequest_Lookup", lookup_start_time, lookup_end_time);^M
//print("Processing request with seqno ", packet.msg.seqno, ". Inside if .\n");^M
- assert r_packet.src !in ref_proposer.highest_seqno_requested_by_client_this_view ||^M
- r_packet.msg.seqno_req > ref_proposer.highest_seqno_requested_by_client_this_view[r_packet.src];^M
+ //assert r_packet.src !in ref_proposer.highest_seqno_requested_by_client_this_view ||^M
+ // r_packet.msg.seqno_req > ref_proposer.highest_seqno_requested_by_client_this_view[r_packet.src];^M
^M
//var map_update_start_time := Time.GetDebugTimeTicks();^M
- var new_seqno_map := proposer.highest_seqno_requested_by_client_this_view[packet.src := packet.msg.seqno];^M
+ var new_seqno_map := proposer.highest_seqno_requested_by_client_this_view;//[packet.src := packet.msg.seqno];^M
//var map_update_end_time := Time.GetDebugTimeTicks();^M
//RecordTimingSeq("ProposerProcessRequest_MapUpdate", map_update_start_time, map_update_end_time);^M
^M
@@ -145,7 +145,7 @@ method {:timeLimitMultiplier 2} ProposerProcessRequest(proposer:ProposerState, p
[request_queue := ref_proposer.request_queue + [ref_val]]^M
[highest_seqno_requested_by_client_this_view := ^M
ref_proposer.highest_seqno_requested_by_client_this_view^M
- [r_packet.src := r_packet.msg.seqno_req]];^M
+ ];//[r_packet.src := r_packet.msg.seqno_req]];^M
ghost var ref_proposer' := AbstractifyProposerStateToLProposer(proposer');^M
assert Eq_LProposer(r_proposer, ref_proposer');^M
assert LProposerProcessRequest(ref_proposer, r_proposer, r_packet);^M
diff --git a/ironfleet/src/Dafny/Distributed/Protocol/RSL/Proposer.i.dfy b/ironfleet/src/Dafny/Distributed/Protocol/RSL/Proposer.i.dfy
index f59ccaa..3828f65 100755
--- a/ironfleet/src/Dafny/Distributed/Protocol/RSL/Proposer.i.dfy
+++ b/ironfleet/src/Dafny/Distributed/Protocol/RSL/Proposer.i.dfy
@@ -155,11 +155,11 @@ predicate LProposerProcessRequest(s:LProposer, s':LProposer, packet:RslPacket)
var val := Request(packet.src, packet.msg.seqno_req, packet.msg.val);
ElectionStateReflectReceivedRequest(s.election_state, s'.election_state, val)
&& if s.current_state != 0
- && ( val.client !in s.highest_seqno_requested_by_client_this_view
+ && (true|| val.client !in s.highest_seqno_requested_by_client_this_view^M
|| val.seqno > s.highest_seqno_requested_by_client_this_view[val.client]) then
s' == s.(election_state := s'.election_state,
request_queue := s.request_queue + [val],
- highest_seqno_requested_by_client_this_view := s.highest_seqno_requested_by_client_this_view[val.client := val.seqno])
+ highest_seqno_requested_by_client_this_view := s.highest_seqno_requested_by_client_this_view) // [val.client := val.seqno])^M
else
s' == s.(election_state := s'.election_state)
}
diff --git a/ironfleet/src/IronfleetClient/IronfleetClient/MultiPaxos.cs b/ironfleet/src/IronfleetClient/IronfleetClient/MultiPaxos.cs
index ffe32cc..791c0c1 100755
--- a/ironfleet/src/IronfleetClient/IronfleetClient/MultiPaxos.cs
+++ b/ironfleet/src/IronfleetClient/IronfleetClient/MultiPaxos.cs
@@ -136,7 +136,7 @@
// seqNum = newSeqNum;
//}
- seq_num++;
+ //seq_num++;^M
var msg = new RequestMessage(seq_num, myaddr);
Trace("Client " + id.ToString() + ": Sending a request with a sequence number " + msg.GetSeqNum() + " to " + ClientBase.endpoints[serverIdx].ToString());
@@ -174,6 +174,7 @@
received_reply = true;
// Report time in milliseconds, since that's what the Python script appears to expect
Console.Out.WriteLine(string.Format("#req{0} {1} {2} {3}", seq_num, (ulong)(start_time * 1.0 / Stopwatch.Frequency * Math.Pow(10, 3)), (ulong)(end_time * 1.0 / Stopwatch.Frequency * Math.Pow(10, 3)), id));
+ Console.Out.WriteLine(string.Format("#req{0} {1}", seq_num, ByteArrayToString(bytes)));^M
//long n = Interlocked.Increment(ref num_reqs);
//if (1 == n || n % 1000 == 0)
//{
Executing the clients with the patch above produces the following result:
#req0 13243 14195 0
#req0 0000000000000006000000000000000000000000000000010000000000000001
#req0 13243 14195 1
#req0 0000000000000006000000000000000000000000000000010000000000000002
#req0 13243 14195 2
#req0 0000000000000006000000000000000000000000000000010000000000000003
#req0 13242 14196 3
#req0 0000000000000006000000000000000000000000000000010000000000000004
#req0 13242 14196 4
#req0 0000000000000006000000000000000000000000000000010000000000000005
#req0 13243 14196 5
#req0 0000000000000006000000000000000000000000000000010000000000000006
#req0 14195 14196 0
#req0 0000000000000006000000000000000000000000000000010000000000000007
#req0 13243 14196 6
#req0 0000000000000006000000000000000000000000000000010000000000000008
#req0 14195 14196 1
#req0 0000000000000006000000000000000000000000000000010000000000000009
#req0 13243 14196 7
#req0 000000000000000600000000000000000000000000000001000000000000000A
#req0 14195 14196 2
#req0 000000000000000600000000000000000000000000000001000000000000000B
#req0 14196 14447 0
#req0 000000000000000600000000000000000000000000000001000000000000000C
As can be seen from the client output, the counter value increases even when the same client sends a request with a repeated sequential number.
I stumbled across this whilst looking for the new ironclad kernel written in Ada.
Ada/Spark is the pinnacle of formal verification tooling. Ada without Spark mode protects against buffer overflows and is as fast as and easier to use than C. Ada also has a distributed computing annex. So why not use that which took decades to design and develop?
When building using scons, it sometimes creates the wrong host executable. For instance, sometimes src/Dafny/Distributed/Services/SHT/build/IronfleetShell.dll will actually be the executable for the lock service, not the SHT service.
This likely arises because the same IronfleetShell.csproj is used to build all three host executables. The ironfleet_shell_lock in SConstruct is supposed to serialize building the executables so that no two host executables are ever being built at the same time. And, indeed, the output from scons suggests that the host executable builds are indeed happening serially, as the lock is intended to ensure. But somehow this doesn't seem to prevent this issue.
I ran into Dafny from a post in https://blog.acolyer.org/2015/10/15/ironfleet-proving-practical-distributed-systems-correc/ which I found to be of great interest. However, I found this repo to be difficult to understand ... there doesn't seem to be well defined boundaries between examples where they start or stop ... it's unclear how to load any of these examples ... I have a sense there's Dafny library code here that might be re-used but that's not entirely clear either. Can we reorg this or can the maintainers give a road map of what this is supposed to communicate?
Somewhat unrelated ... does Dafny come with Verdi's formally proved library which represents error free, exactly once delivery of messages, or possibly droppep/dup messages? See https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-pldi15.pdf for the description there. Also see: https://github.com/uwplse/verdi. Dafny seems to go further than other formal tools at continuously refining down from spec to more runnable code and it'd be a shame to let this work flounder. Verdi also wants to improve here, but Verdi doesn't do liveness checks.
Finally, is Dafny supposed to be a model checker ala SPIN/TLA+ or proof oriented ala Coq/Verdi? Dafny seems to be proof oriented.
Regards
Verifying the current Ironfleet head (c07cd96) from the console produces several “inconclusive” verification errors.
Here is an example of the errors produced:
src\Dafny\Distributed\Common\Logic\Temporal\Rules.i.dfy(191,10): Verification inconclusive (CheckWellformed$$_9_Temporal____Rules__i.__default.Lemma__AlwaysImpliesLaterAlways)
Prover error: Error setting 'smt.arith.nl', reason: unknown option.
Prover error: ERROR: invalid INI file
Prover error: Prover died
If the Z3 binary (version 4.1) included with Ironfleet is replaced with a more recent version of Z3 that I had around (version 4.4.1 - 64 bit) everything works correctly on my machine.
There are important files that Microsoft projects should all have that are not present in this repository. A pull request has been opened to add the missing file(s). When the pr is merged this issue will be closed automatically.
Microsoft teams can learn more about this effort and share feedback within the open source guidance available internally.
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.