Merge branch 'main' into tla-docs-page

doc/research/index.rst

@@ -1,7 +1,7 @@
 Research
 ========
 
-2023: `Confidential Consortium Framework: Secure Multiparty Applications with Confidentiality, Integrity, and High Availability <aka.ms/ccf-paper>`_
+2023: `Confidential Consortium Framework: Secure Multiparty Applications with Confidentiality, Integrity, and High Availability <https://aka.ms/ccf-paper>`_
  Confidentiality, integrity protection, and high availability, abbreviated to CIA, are essential properties for trustworthy data systems. The rise of cloud computing and the growing demand for multiparty applications however means that building modern CIA systems is more challenging than ever. In response, we present the Confidential Consortium Framework (CCF), a general-purpose foundation for developing secure stateful CIA applications. CCF combines centralized compute with decentralized trust, supporting deployment on untrusted cloud infrastructure and transparent governance by mutually untrusted parties.
 
  CCF leverages hardware-based trusted execution environments for remotely verifiable confidentiality and code integrity. This is coupled with state machine replication backed by an auditable immutable ledger for data integrity and high availability. CCF enables each service to bring its own application logic, custom multiparty governance model, and deployment scenario, decoupling the operators of nodes from the consortium that governs them.

tla/consensus/MCccfraft.cfg

@@ -10,6 +10,7 @@ CONSTANTS
     Timeout <- MCTimeout
     Send <- MCSend
     ClientRequest <- MCClientRequest
+    SignCommittableMessages <- MCSignCommittableMessages
     ChangeConfigurationInt <- MCChangeConfigurationInt
     NotifyCommit <- MCNotifyCommit
 

tla/consensus/MCccfraft.tla

@@ -55,6 +55,14 @@ MCClientRequest(i) ==
     /\ FoldSeq(LAMBDA e, count: IF e.contentType = TypeEntry THEN count + 1 ELSE count, 0, log[i]) < RequestLimit
     /\ CCF!ClientRequest(i)
 
+MCSignCommittableMessages(i) ==
+    \* The implementation periodically emits a signature for the current log, potentially causing consecutive
+    \* signatures.  However, modeling consecutive sigs would result in a state space explosion, i.e., an infinite
+    \* number of states.  Thus, we prevent a leader from creating consecutive sigs.  We assume that consecutive
+    \* sigs will not violate safety or liveness.
+    /\ log[i] # <<>> => Last(log[i]).contentType # TypeSignature
+    /\ CCF!SignCommittableMessages(i)
+
 \* CCF: Limit how many identical append entries messages each node can send to another
 \* Limit number of duplicate messages sent to the same server
 MCSend(msg) ==

tla/consensus/MCccfraftWithReconfig.cfg

@@ -10,6 +10,7 @@ CONSTANTS
     Timeout <- MCTimeout
     Send <- MCSend
     ClientRequest <- MCClientRequest
+    SignCommittableMessages <- MCSignCommittableMessages
     ChangeConfigurationInt <- MCChangeConfigurationInt
     NotifyCommit <- MCNotifyCommit
 

tla/consensus/ccfraft.tla

@@ -642,15 +642,15 @@ ClientRequest(i) ==
 \* In CCF, the leader periodically signs the latest log prefix. Only these signatures are committable in CCF.
 \* We model this via special ``TypeSignature`` log entries and ensure that the commitIndex can only be moved to these special entries.
 
-\* Leader i signs the previous messages in its log to make them committable
-\* This is done as a separate entry in the log that has a different
-\* message contentType than messages entered by the client.
+\* Leader i signs the previous entries in its log to make them committable.
+\* This is done as a separate entry in the log that has contentType Signature
+\* compared to ordinary entries with contentType Entry.
+\* See history::start_signature_emit_timer
 SignCommittableMessages(i) ==
-    \* Only applicable to Leaders with a log that contains at least one message
+    \* Only applicable to Leaders with a log that contains at least one entry.
     /\ state[i] = Leader
+    \* The first log entry cannot be a signature.
     /\ log[i] # << >>
-    \* Make sure the leader does not create two signatures in a row
-    /\ Last(log[i]).contentType # TypeSignature
     \* Create a new entry in the log that has the contentType Signature and append it
     /\ log' = [log EXCEPT ![i] = @ \o <<[term  |-> currentTerm[i], contentType  |-> TypeSignature]>>]
     /\ committableIndices' = [ committableIndices EXCEPT ![i] = @ \cup {Len(log'[i])} ]