diff --git a/.azure-pipelines-gh-pages.yml b/.azure-pipelines-gh-pages.yml index ffa61b30a837..76868d7470c4 100644 --- a/.azure-pipelines-gh-pages.yml +++ b/.azure-pipelines-gh-pages.yml @@ -11,7 +11,7 @@ jobs: variables: Codeql.SkipTaskAutoInjection: true skipComponentGovernanceDetection: true - container: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-virtual-clang15 + container: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-virtual-clang15 pool: vmImage: ubuntu-20.04 diff --git a/.azure-pipelines-release.yml b/.azure-pipelines-release.yml index 161007f6b5c8..9a1d5c664c8f 100644 --- a/.azure-pipelines-release.yml +++ b/.azure-pipelines-release.yml @@ -8,15 +8,15 @@ pr: none resources: containers: - container: virtual - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-virtual-clang15 + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-virtual-clang15 options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro - container: snp - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-snp-clang15 + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-snp-clang15 options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro - container: sgx - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-sgx + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-sgx options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --device /dev/sgx_enclave:/dev/sgx_enclave --device /dev/sgx_provision:/dev/sgx_provision -v /dev/sgx:/dev/sgx -v /lib/modules:/lib/modules:ro variables: diff --git a/.azure-pipelines-templates/deploy_aci.yml b/.azure-pipelines-templates/deploy_aci.yml index 1560094580fe..ce06ddea2519 100644 --- a/.azure-pipelines-templates/deploy_aci.yml +++ b/.azure-pipelines-templates/deploy_aci.yml @@ -51,7 +51,7 @@ jobs: - script: | set -ex docker login -u $ACR_TOKEN_NAME -p $ACR_CI_PUSH_TOKEN_PASSWORD $ACR_REGISTRY - docker pull $ACR_REGISTRY/ccf/ci:25-01-2024-snp-clang15 + docker pull $ACR_REGISTRY/ccf/ci:12-02-2024-snp-clang15 docker build -f docker/ccf_ci_built . --build-arg="base=$BASE_IMAGE" --build-arg="platform=snp" -t $ACR_REGISTRY/ccf/ci:pr-`git rev-parse HEAD` docker push $ACR_REGISTRY/ccf/ci:pr-`git rev-parse HEAD` name: build_ci_image @@ -60,7 +60,7 @@ jobs: ACR_TOKEN_NAME: ci-push-token ACR_CI_PUSH_TOKEN_PASSWORD: $(ACR_CI_PUSH_TOKEN_PASSWORD) ACR_REGISTRY: ccfmsrc.azurecr.io - BASE_IMAGE: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-snp-clang15 + BASE_IMAGE: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-snp-clang15 - script: | set -ex diff --git a/.azure-pipelines-templates/trace_validation.yml b/.azure-pipelines-templates/trace_validation.yml index 6ea5cb054341..77a26f9109b7 100644 --- a/.azure-pipelines-templates/trace_validation.yml +++ b/.azure-pipelines-templates/trace_validation.yml @@ -10,11 +10,13 @@ steps: set -ex set -o pipefail cd tla/ - parallel 'JSON={} java -XX:+UseParallelGC -Dtlc2.tool.impl.Tool.cdot=true -Dtlc2.tool.queue.IStateQueue=StateDeque -cp tla2tools.jar:CommunityModules-deps.jar tlc2.TLC -lncheck final -checkpoint 0 -dump dot,constrained,colorize,actionlabels {}.dot consensus/Traceccfraft.tla' ::: $(ls ../build/*.ndjson | grep -v _deprecated) + mkdir traces + cp ../build/*.ndjson traces/ + parallel 'set -o pipefail && echo {} && JVM_OPTIONS=-Dtlc2.tool.queue.IStateQueue=StateDeque JSON={} ./tlc.sh -dump dot,constrained,colorize,actionlabels {}.dot -dumpTrace tla {}.trace.tla -dumpTrace json {}.trace.json consensus/Traceccfraft.tla | ./last_line.sh {}.trace.json' ::: $(ls traces/*.ndjson) displayName: "Run trace validation" - task: PublishPipelineArtifact@1 inputs: artifactName: "Trace Validation Output" - targetPath: tla + targetPath: tla/traces condition: or(failed(), canceled()) diff --git a/.azure-pipelines.yml b/.azure-pipelines.yml index 0f574d3965d6..1d932d26d8ad 100644 --- a/.azure-pipelines.yml +++ b/.azure-pipelines.yml @@ -30,15 +30,15 @@ schedules: resources: containers: - container: virtual - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-virtual-clang15 + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-virtual-clang15 options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro - container: snp - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-snp-clang15 + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-snp-clang15 options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro - container: sgx - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-sgx + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-sgx options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --device /dev/sgx_enclave:/dev/sgx_enclave --device /dev/sgx_provision:/dev/sgx_provision -v /dev/sgx:/dev/sgx -v /lib/modules:/lib/modules:ro variables: diff --git a/.azure_pipelines_snp.yml b/.azure_pipelines_snp.yml index 5039d002f129..d96643446d43 100644 --- a/.azure_pipelines_snp.yml +++ b/.azure_pipelines_snp.yml @@ -32,7 +32,7 @@ schedules: resources: containers: - container: virtual - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-virtual-clang15 + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-virtual-clang15 options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro jobs: diff --git a/.daily.yml b/.daily.yml index f06505f85547..d46d4b578c49 100644 --- a/.daily.yml +++ b/.daily.yml @@ -27,15 +27,15 @@ schedules: resources: containers: - container: virtual - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-virtual-clang15 + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-virtual-clang15 options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE - container: snp - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-snp-clang15 + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-snp-clang15 options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro - container: sgx - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-sgx + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-sgx options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --device /dev/sgx_enclave:/dev/sgx_enclave --device /dev/sgx_provision:/dev/sgx_provision -v /dev/sgx:/dev/sgx jobs: diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index abf1e7b69f95..2268b2f5d374 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -1,6 +1,6 @@ { "name": "CCF Development Environment", - "image": "ccfmsrc.azurecr.io/ccf/ci:25-01-2024-virtual-clang15", + "image": "ccfmsrc.azurecr.io/ccf/ci:12-02-2024-virtual-clang15", "runArgs": [], "extensions": [ "eamodio.gitlens", diff --git a/.github/workflows/ci-checks.yml b/.github/workflows/ci-checks.yml index ceb321fece40..47bd59187493 100644 --- a/.github/workflows/ci-checks.yml +++ b/.github/workflows/ci-checks.yml @@ -11,7 +11,7 @@ permissions: read-all jobs: checks: runs-on: ubuntu-latest - container: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-virtual-clang15 + container: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-virtual-clang15 steps: - run: git config --global --add safe.directory "$GITHUB_WORKSPACE" diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml index 2983cad442f1..73c0be59cd6e 100644 --- a/.github/workflows/tlaplus.yml +++ b/.github/workflows/tlaplus.yml @@ -16,7 +16,7 @@ jobs: name: Model Checking - Consistency runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub] container: - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-virtual-clang15 + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-virtual-clang15 steps: - uses: actions/checkout@v3 diff --git a/.multi-thread.yml b/.multi-thread.yml index 8b5ca06a94b4..18c312e832cf 100644 --- a/.multi-thread.yml +++ b/.multi-thread.yml @@ -20,7 +20,7 @@ pr: resources: containers: - container: virtual - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-virtual-clang15 + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-virtual-clang15 options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE -v /lib/modules:/lib/modules:ro jobs: diff --git a/.stress.yml b/.stress.yml index 4edd5559f429..c56bbb74b6c5 100644 --- a/.stress.yml +++ b/.stress.yml @@ -24,7 +24,7 @@ schedules: resources: containers: - container: sgx - image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-sgx + image: ccfmsrc.azurecr.io/ccf/ci:12-02-2024-sgx options: --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --device /dev/sgx_enclave:/dev/sgx_enclave --device /dev/sgx_provision:/dev/sgx_provision -v /dev/sgx:/dev/sgx jobs: diff --git a/docker/ccf_ci_built b/docker/ccf_ci_built index 852072d89d48..d7e29a77d8fb 100644 --- a/docker/ccf_ci_built +++ b/docker/ccf_ci_built @@ -4,7 +4,7 @@ # Latest image as of this change ARG platform=sgx -ARG base=ccfmsrc.azurecr.io/ccf/ci:25-01-2024-snp-clang-15 +ARG base=ccfmsrc.azurecr.io/ccf/ci:12-02-2024-snp-clang-15 FROM ${base} # SSH. Note that this could (should) be done in the base ccf_ci image instead diff --git a/include/ccf/crypto/entropy.h b/include/ccf/crypto/entropy.h index e211d7a88121..7641627d941f 100644 --- a/include/ccf/crypto/entropy.h +++ b/include/ccf/crypto/entropy.h @@ -303,6 +303,5 @@ namespace crypto using EntropyPtr = std::shared_ptr; static EntropyPtr intel_drng_ptr; - /** Create a default Entropy object */ - EntropyPtr create_entropy(); + EntropyPtr get_entropy(); } diff --git a/include/ccf/crypto/symmetric_key.h b/include/ccf/crypto/symmetric_key.h index 8cc1f5639f97..fcf25ba8e606 100644 --- a/include/ccf/crypto/symmetric_key.h +++ b/include/ccf/crypto/symmetric_key.h @@ -44,7 +44,7 @@ namespace crypto return GCM_SIZE_TAG + IV_SIZE; } - void set_random_iv(EntropyPtr entropy = crypto::create_entropy()) + void set_random_iv(EntropyPtr entropy = crypto::get_entropy()) { iv = entropy->random(IV_SIZE); } diff --git a/scripts/azure_deployment/arm_aci.py b/scripts/azure_deployment/arm_aci.py index 21b0686635dc..0b33f2de4636 100644 --- a/scripts/azure_deployment/arm_aci.py +++ b/scripts/azure_deployment/arm_aci.py @@ -133,7 +133,7 @@ def parse_aci_args(parser: ArgumentParser) -> Namespace: "--aci-image", help="The name of the image to deploy in the ACI", type=str, - default="ccfmsrc.azurecr.io/ccf/ci:25-01-2024-snp", + default="ccfmsrc.azurecr.io/ccf/ci:12-02-2024-snp", ) parser.add_argument( "--aci-type", diff --git a/src/consensus/aft/raft.h b/src/consensus/aft/raft.h index 50491771439a..d492b7c91c4f 100644 --- a/src/consensus/aft/raft.h +++ b/src/consensus/aft/raft.h @@ -296,16 +296,29 @@ namespace aft return state->membership_state == kv::MembershipState::Retired; } - void set_retired_committed(ccf::SeqNo seqno) override - { - state->retirement_phase = kv::RetirementPhase::RetiredCommitted; - CCF_ASSERT_FMT( - state->retired_committed_idx == state->commit_idx, - "Retired " - "committed index {} does not match current commit index {}", - state->retired_committed_idx.value_or(0), - state->commit_idx); - state->retired_committed_idx = seqno; + void set_retired_committed( + ccf::SeqNo seqno, const std::vector& node_ids) override + { + for (auto& node_id : node_ids) + { + if (id() == node_id) + { + CCF_ASSERT( + state->membership_state == kv::MembershipState::Retired, + "Node is not retired, cannot become retired committed"); + CCF_ASSERT( + state->retirement_phase == kv::RetirementPhase::Completed, + "Node is not retired, cannot become retired committed"); + CCF_ASSERT_FMT( + state->retired_committed_idx == state->commit_idx, + "Retired " + "committed index {} does not match current commit index {}", + state->retired_committed_idx.value_or(0), + state->commit_idx); + state->retirement_phase = kv::RetirementPhase::RetiredCommitted; + state->retired_committed_idx = seqno; + } + } } Index last_committable_index() const @@ -1981,54 +1994,58 @@ namespace aft } else if (phase == kv::RetirementPhase::Completed) { - leader_id.reset(); - state->leadership_state = kv::LeadershipState::None; - ProposeRequestVote prv{.term = state->current_view}; - - std::optional successor = std::nullopt; - Index max_match_idx = 0; - kv::ReconfigurationId reconf_id_of_max_match = 0; - - // Pick the node that has the highest match_idx, and break - // ties by looking at the highest reconfiguration id they are - // part of. This can lead to nudging a node that is - // about to retire too, but that node will then nudge - // a successor, and that seems preferable to nudging a node that - // risks not being eligible if reconfiguration id is prioritised. - // Alternatively, we could pick the node with the higest match idx - // in the latest config, provided that match idx at least as high as a - // majority. That would make them both eligible and unlikely to retire - // soon. - for (auto& [node, node_state] : all_other_nodes) + if (state->leadership_state == kv::LeadershipState::Leader) { - if (node_state.match_idx >= max_match_idx) + ProposeRequestVote prv{.term = state->current_view}; + + std::optional successor = std::nullopt; + Index max_match_idx = 0; + kv::ReconfigurationId reconf_id_of_max_match = 0; + + // Pick the node that has the highest match_idx, and break + // ties by looking at the highest reconfiguration id they are + // part of. This can lead to nudging a node that is + // about to retire too, but that node will then nudge + // a successor, and that seems preferable to nudging a node that + // risks not being eligible if reconfiguration id is prioritised. + // Alternatively, we could pick the node with the higest match idx + // in the latest config, provided that match idx at least as high as a + // majority. That would make them both eligible and unlikely to retire + // soon. + for (auto& [node, node_state] : all_other_nodes) { - kv::ReconfigurationId latest_reconf_id = 0; - auto conf = configurations.rbegin(); - while (conf != configurations.rend()) + if (node_state.match_idx >= max_match_idx) { - if (conf->nodes.find(node) != conf->nodes.end()) + kv::ReconfigurationId latest_reconf_id = 0; + auto conf = configurations.rbegin(); + while (conf != configurations.rend()) { - latest_reconf_id = conf->idx; - break; + if (conf->nodes.find(node) != conf->nodes.end()) + { + latest_reconf_id = conf->idx; + break; + } + conf++; + } + if (!(node_state.match_idx == max_match_idx && + latest_reconf_id < reconf_id_of_max_match)) + { + reconf_id_of_max_match = latest_reconf_id; + successor = node; + max_match_idx = node_state.match_idx; } - conf++; - } - if (!(node_state.match_idx == max_match_idx && - latest_reconf_id < reconf_id_of_max_match)) - { - reconf_id_of_max_match = latest_reconf_id; - successor = node; - max_match_idx = node_state.match_idx; } } + if (successor.has_value()) + { + RAFT_INFO_FMT("Node retired, nudging {}", successor.value()); + channels->send_authenticated( + successor.value(), ccf::NodeMsgType::consensus_msg, prv); + } } - if (successor.has_value()) - { - RAFT_INFO_FMT("Node retired, nudging {}", successor.value()); - channels->send_authenticated( - successor.value(), ccf::NodeMsgType::consensus_msg, prv); - } + + leader_id.reset(); + state->leadership_state = kv::LeadershipState::None; } state->membership_state = kv::MembershipState::Retired; diff --git a/src/consensus/aft/test/driver.h b/src/consensus/aft/test/driver.h index c15b0a8972d2..e37ec943402c 100644 --- a/src/consensus/aft/test/driver.h +++ b/src/consensus/aft/test/driver.h @@ -198,7 +198,9 @@ class RaftDriver std::make_shared(node_id), nullptr); kv->set_set_retired_committed_hook( - [&raft](aft::Index idx) { raft->set_retired_committed(idx); }); + [raft](aft::Index idx, const std::vector& node_ids) { + raft->set_retired_committed(idx, node_ids); + }); raft->start_ticking(); if (_nodes.find(node_id) != _nodes.end()) diff --git a/src/consensus/aft/test/logging_stub.h b/src/consensus/aft/test/logging_stub.h index b45ebfcf75cf..b7c42e7ac1cd 100644 --- a/src/consensus/aft/test/logging_stub.h +++ b/src/consensus/aft/test/logging_stub.h @@ -329,17 +329,19 @@ namespace aft } }; + using RCHook = std::function&)>; + class LoggingStubStore { protected: ccf::NodeId _id; - std::function set_retired_committed_hook; + RCHook set_retired_committed_hook; public: LoggingStubStore(ccf::NodeId id) : _id(id) {} virtual void set_set_retired_committed_hook( - std::function set_retired_committed_hook_) + RCHook set_retired_committed_hook_) { set_retired_committed_hook = set_retired_committed_hook_; } @@ -480,16 +482,12 @@ namespace aft { if (version <= i) { - std::cout << "Retired committed configuration: " - << configuration.dump() << std::endl; - if (configuration.find(_id) != configuration.end()) + std::vector retired_committed_node_ids; + for (auto& [node_id, _] : configuration.items()) { - std::cout << "Node id: " << _id - << " is in the retired committed configuration, calling " - "set_retired_committed hook" - << std::endl; - set_retired_committed_hook(i); + retired_committed_node_ids.push_back(node_id); } + set_retired_committed_hook(i, retired_committed_node_ids); } else { diff --git a/src/crypto/entropy.cpp b/src/crypto/entropy.cpp index 3f04be3cd32c..8a1dbcc48ab0 100644 --- a/src/crypto/entropy.cpp +++ b/src/crypto/entropy.cpp @@ -7,7 +7,7 @@ namespace crypto { - EntropyPtr create_entropy() + EntropyPtr get_entropy() { if (use_drng) { diff --git a/src/crypto/sharing.cpp b/src/crypto/sharing.cpp index ecf76fa27c76..32bd3ecd95b3 100644 --- a/src/crypto/sharing.cpp +++ b/src/crypto/sharing.cpp @@ -8,177 +8,205 @@ namespace crypto { - /* PRIME FIELD - - For simplicity, we use a finite field F[prime] where all operations - are defined in plain uint64_t arithmetic, and we reduce after every - operation. This is not meant to be efficient. Compared to e.g. GF(2^n), the - main drawback is that we need to hash the "raw secret" to obtain a - uniformly-distributed secret. - */ - - using element = uint64_t; - constexpr element prime = (1ul << 31) - 1ul; // a notorious Mersenne prime - - static element reduce(uint64_t x) - { - return (x % prime); - } - - static element mul(element x, element y) - { - return ((x * y) % prime); - } - - static element add(element x, element y) + namespace sharing { - return ((x + y) % prime); - } - - static element sub(element x, element y) - { - return ((prime + x - y)) % prime; - } - - // naive algorithm, used only to compute coefficients, not for use on secrets! - static element exp(element x, size_t n) - { - element y = 1; - while (n > 0) + /* PRIME FIELD + + For simplicity, we use a finite field F[prime] where all operations + are defined in plain uint64_t arithmetic, and we reduce after every + operation. This is not meant to be efficient. Compared to e.g. GF(2^n), + the main drawback is that we need to hash the "raw secret" to obtain a + uniformly-distributed secret. + */ + + using element = uint64_t; + constexpr element prime = (1ul << 31) - 1ul; // a notorious Mersenne prime + /* + Constant time version of: + static element reduce(element x) + { + return (x % prime); + } + Instructions checked against list published by Intel at: + https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/resources/data-operand-independent-timing-instructions.html + Note that IA32_UARCH_MISC_CTL[DOITM] must be set for this to be guaranteed, + as per: + https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/best-practices/data-operand-independent-timing-isa-guidance.html + This is always the case in SGX, but may not be true elsewhere. + */ + element ct_reduce(element x) { - if (n & 1) - y = mul(y, x); - x = mul(x, x); - n >>= 1; + // initially, x < 2^64 + // we compute under-approximations x/(2^31) of x/prime + uint64_t d; + d = x >> 31; + x -= d * prime; + // after this first reduction, x <= 5*prime + 3 + d = x >> 31; + x -= d * prime; + // after this second reduction, x <= prime + 3 + d = (x + 1) >> 31; + x -= d * prime; + // d is correct for every x in this range + return x; } - return y; - } - static element inv(element x) - { - if (x == 0) + static element mul(element x, element y) { - throw std::invalid_argument("division by zero"); + return ct_reduce(x * y); } - return exp(x, prime - 2); - } - - // This function is specific to prime=2^31-1. - // We assume the lower 31 bits are uniformly distributed, - // and retry if they are all set to get uniformity in F[prime]. - static element sample(const crypto::EntropyPtr& entropy) - { - uint64_t res = prime; - while (res == prime) + static element add(element x, element y) { - res = entropy->random64() & prime; + return ct_reduce(x + y); } - return res; - } - /* POLYNOMIAL SHARING AND INTERPOLATION */ - - static void sample_polynomial( - element p[], size_t degree, const crypto::EntropyPtr& entropy) - { - for (size_t i = 0; i <= degree; i++) + static element sub(element x, element y) { - p[i] = sample(entropy); + return ct_reduce(prime + x - y); } - } - static element eval(element p[], size_t degree, element x) - { - element y = 0, x_i = 1; - for (size_t i = 0; i <= degree; i++) + // naive algorithm, used only to compute coefficients, not for use on + // secrets! + static element exp(element x, size_t n) { - // x_i == x^i - y = add(y, mul(p[i], x_i)); - x_i = mul(x, x_i); + element y = 1; + while (n > 0) + { + if (n & 1) + y = mul(y, x); + x = mul(x, x); + n >>= 1; + } + return y; } - return y; - } - void sample_secret_and_shares( - Share& raw_secret, const std::span& shares, size_t threshold) - { - if (shares.size() < 1) + static element inv(element x) { - throw std::invalid_argument("insufficient number of shares"); + if (x == 0) + { + throw std::invalid_argument("division by zero"); + } + return exp(x, prime - 2); } - if (threshold < 1 || threshold > shares.size()) + // This function is specific to prime=2^31-1. + // We assume the lower 31 bits are uniformly distributed, + // and retry if they are all set to get uniformity in F[prime]. + + static element sample(const crypto::EntropyPtr& entropy) { - throw std::invalid_argument("invalid threshold"); + uint64_t res = prime; + while (res == prime) + { + res = entropy->random64() & prime; + } + return res; } - size_t degree = threshold - 1; + /* POLYNOMIAL SHARING AND INTERPOLATION */ - raw_secret.x = 0; - for (size_t s = 0; s < shares.size(); s++) + static void sample_polynomial( + element p[], size_t degree, const crypto::EntropyPtr& entropy) { - shares[s].x = s + 1; + for (size_t i = 0; i <= degree; i++) + { + p[i] = sample(entropy); + } } - auto entropy = crypto::create_entropy(); - - for (size_t limb = 0; limb < LIMBS; limb++) + static element eval(element p[], size_t degree, element x) { - element p[degree + 1]; /*SECRET*/ - sample_polynomial(p, degree, entropy); - raw_secret.y[limb] = p[0]; - for (size_t s = 0; s < shares.size(); s++) + element y = 0, x_i = 1; + for (size_t i = 0; i <= degree; i++) { - shares[s].y[limb] = eval(p, degree, shares[s].x); + // x_i == x^i + y = add(y, mul(p[i], x_i)); + x_i = mul(x, x_i); } + return y; } - } - void recover_unauthenticated_secret( - Share& raw_secret, const std::span& shares, size_t threshold) - { - if (shares.size() < threshold) + void sample_secret_and_shares( + Share& raw_secret, const std::span& shares, size_t threshold) { - throw std::invalid_argument("insufficient input shares"); - } - // We systematically reduce the input shares instead of checking they are - // well-formed. + if (shares.size() < 1) + { + throw std::invalid_argument("insufficient number of shares"); + } - size_t degree = threshold - 1; + if (threshold < 1 || threshold > shares.size()) + { + throw std::invalid_argument("invalid threshold"); + } - // Precomputes Lagrange coefficients for interpolating p(0). No secrets - // involved. - element lagrange[degree + 1]; - for (size_t i = 0; i <= degree; i++) - { - element numerator = 1, denominator = 1; - for (size_t j = 0; j <= degree; j++) + size_t degree = threshold - 1; + + raw_secret.x = 0; + for (size_t s = 0; s < shares.size(); s++) { - if (i != j) - { - numerator = mul(numerator, reduce(shares[j].x)); - denominator = - mul(denominator, sub(reduce(shares[j].x), reduce(shares[i].x))); - } + shares[s].x = s + 1; } - if (denominator == 0) + + auto entropy = crypto::get_entropy(); + + for (size_t limb = 0; limb < LIMBS; limb++) { - throw std::invalid_argument("duplicate input share"); + element p[degree + 1]; /*SECRET*/ + sample_polynomial(p, degree, entropy); + raw_secret.y[limb] = p[0]; + for (size_t s = 0; s < shares.size(); s++) + { + shares[s].y[limb] = eval(p, degree, shares[s].x); + } } - lagrange[i] = mul(numerator, inv(denominator)); } - // Interpolate every limb of the secret. Constant-time on y values. - raw_secret.x = 0; - for (size_t limb = 0; limb < LIMBS; limb++) + void recover_unauthenticated_secret( + Share& raw_secret, const std::span& shares, size_t threshold) { - element y = 0; + if (shares.size() < threshold) + { + throw std::invalid_argument("insufficient input shares"); + } + // We systematically reduce the input shares instead of checking they are + // well-formed. + + size_t degree = threshold - 1; + + // Precomputes Lagrange coefficients for interpolating p(0). No secrets + // involved. + element lagrange[degree + 1]; for (size_t i = 0; i <= degree; i++) { - y = add(y, mul(lagrange[i], reduce(shares[i].y[limb]))); + element numerator = 1, denominator = 1; + for (size_t j = 0; j <= degree; j++) + { + if (i != j) + { + numerator = mul(numerator, ct_reduce(shares[j].x)); + denominator = mul( + denominator, sub(ct_reduce(shares[j].x), ct_reduce(shares[i].x))); + } + } + if (denominator == 0) + { + throw std::invalid_argument("duplicate input share"); + } + lagrange[i] = mul(numerator, inv(denominator)); + } + + // Interpolate every limb of the secret. Constant-time on y values. + raw_secret.x = 0; + for (size_t limb = 0; limb < LIMBS; limb++) + { + element y = 0; + for (size_t i = 0; i <= degree; i++) + { + y = add(y, mul(lagrange[i], ct_reduce(shares[i].y[limb]))); + } + raw_secret.y[limb] = y; } - raw_secret.y[limb] = y; } } } diff --git a/src/crypto/sharing.h b/src/crypto/sharing.h index ce749b34aef2..4a3c225d2991 100644 --- a/src/crypto/sharing.h +++ b/src/crypto/sharing.h @@ -16,102 +16,113 @@ namespace crypto { - // We get (almost) 31 bits of entropy per limb, hence to get 256 bits of - // entropy of derived key material, with 80 bits of safety margin, - // ((256+80)/31) = 10 limbs. - static constexpr size_t LIMBS = 10; - static constexpr const char* key_label = "CCF Wrapping Key v1"; - - struct Share + namespace sharing { - // Index in a re-share, 0 is a full key, and 1+ is a partial share - uint32_t x = 0; - uint32_t y[LIMBS]; - constexpr static size_t serialised_size = - sizeof(uint32_t) + sizeof(uint32_t) * LIMBS; - - Share() = default; - bool operator==(const Share& other) const = default; + // We get (almost) 31 bits of entropy per limb, hence to get 256 bits of + // entropy of derived key material, with 80 bits of safety margin, + // ((256+80)/31) = 10 limbs. + static constexpr size_t LIMBS = 10; + static constexpr const char* key_label = "CCF Wrapping Key v1"; - ~Share() + struct Share { - OPENSSL_cleanse(y, sizeof(y)); - }; + // Index in a re-share, 0 is a full key, and 1+ is a partial share + uint32_t x = 0; + uint32_t y[LIMBS]; + constexpr static size_t serialised_size = + sizeof(uint32_t) + sizeof(uint32_t) * LIMBS; - HashBytes key(size_t key_size) const - { - if (x != 0) + Share() = default; + bool operator==(const Share& other) const = default; + + ~Share() + { + OPENSSL_cleanse(y, sizeof(y)); + }; + + HashBytes key(size_t key_size) const { - throw std::invalid_argument("Cannot derive a key from a partial share"); + if (x != 0) + { + throw std::invalid_argument( + "Cannot derive a key from a partial share"); + } + const std::span ikm( + reinterpret_cast(y), sizeof(y)); + const std::span label( + reinterpret_cast(y), sizeof(y)); + auto k = crypto::hkdf(crypto::MDType::SHA256, key_size, ikm, {}, label); + return k; } - const std::span ikm( - reinterpret_cast(y), sizeof(y)); - const std::span label( - reinterpret_cast(y), sizeof(y)); - auto k = crypto::hkdf(crypto::MDType::SHA256, key_size, ikm, {}, label); - return k; - } - std::vector serialise() const - { - auto size = serialised_size; - std::vector serialised(size); - auto data = serialised.data(); - serialized::write(data, size, x); - for (size_t i = 0; i < LIMBS; ++i) + std::vector serialise() const { - serialized::write(data, size, y[i]); + auto size = serialised_size; + std::vector serialised(size); + auto data = serialised.data(); + serialized::write(data, size, x); + for (size_t i = 0; i < LIMBS; ++i) + { + serialized::write(data, size, y[i]); + } + return serialised; } - return serialised; - } - Share(const std::span& serialised) - { - if (serialised.size() != serialised_size) + Share(const std::span& serialised) { - throw std::invalid_argument("Invalid serialised share size"); + if (serialised.size() != serialised_size) + { + throw std::invalid_argument("Invalid serialised share size"); + } + auto data = serialised.data(); + auto size = serialised.size(); + x = serialized::read(data, size); + for (size_t i = 0; i < LIMBS; ++i) + { + y[i] = serialized::read(data, size); + } } - auto data = serialised.data(); - auto size = serialised.size(); - x = serialized::read(data, size); - for (size_t i = 0; i < LIMBS; ++i) + + std::string to_str() const { - y[i] = serialized::read(data, size); + return fmt::format("x: {} y: {}", x, fmt::join(y, ", ")); } - } + }; - std::string to_str() const - { - return fmt::format("x: {} y: {}", x, fmt::join(y, ", ")); - } - }; + // Exposed for testing only + using element = uint64_t; + element ct_reduce(element x); - /** Sample a secret into @p raw_secret, and split it into @p shares. - * Enforces 1 < @p threshold <= number of shares. - * - * @param[out] raw_secret Sampled secret value. - * @param[out] shares Shares of raw_secret. Note that the size of the span - * determines the number of shares. - * @param[in] threshold Number of shares necessary to recover the secret. - * - * The secret is guaranteed to contain at least 256 bits of entropy. - * Note that is it not safe to use the secret as a key directly, - * and that a round of key derivation is necessary (Share::key()). - */ - void sample_secret_and_shares( - Share& raw_secret, const std::span& shares, size_t threshold); + /** Sample a secret into @p raw_secret, and split it into @p shares. + * Enforces 1 < @p threshold <= number of shares. + * + * @param[out] raw_secret Sampled secret value. + * @param[out] shares Shares of raw_secret. Note that the size of the span + * determines the number of shares. + * @param[in] threshold Number of shares necessary to recover the secret. + * + * The secret is guaranteed to contain at least 256 bits of entropy. + * Note that is it not safe to use the secret as a key directly, + * and that a round of key derivation is necessary (Share::key()). + */ + void sample_secret_and_shares( + Share& raw_secret, const std::span& shares, size_t threshold); - /** Using @p shares, recover @p secret, without authentication. - * - * @param[out] raw_secret Recovered secret value. - * @param[in] shares Shares of raw_secret. - * @param threshold Number of shares necessary to recover the secret. - * - * Note that shares passed in excess of the threshold are ignored. - * - * @throws std::invalid_argument if the number of shares is insufficient, - * or if two shares have the same x coordinate. - */ - void recover_unauthenticated_secret( - Share& raw_secret, const std::span& shares, size_t threshold); + /** Using @p shares, recover @p secret, without authentication. + * + * @param[out] raw_secret Recovered secret value. + * @param[in] shares Shares of raw_secret. + * @param threshold Number of shares necessary to recover the secret. + * + * Note that shares passed in excess of the threshold are ignored, + * and that recovery does not authenticate the shares or the threshold. + * + * @throws std::invalid_argument if the number of shares is insufficient, + * or if two shares have the same x coordinate. + */ + void recover_unauthenticated_secret( + Share& raw_secret, + const std::span& shares, + size_t threshold); + } } \ No newline at end of file diff --git a/src/crypto/test/bench.cpp b/src/crypto/test/bench.cpp index a79a142a21fd..089069f2fba0 100644 --- a/src/crypto/test/bench.cpp +++ b/src/crypto/test/bench.cpp @@ -97,8 +97,7 @@ template static void benchmark_hmac(picobench::state& s) { const auto contents = make_contents(); - const auto key = - crypto::create_entropy()->random(crypto::GCM_DEFAULT_KEY_SIZE); + const auto key = crypto::get_entropy()->random(crypto::GCM_DEFAULT_KEY_SIZE); s.start_timer(); for (auto _ : s) @@ -474,7 +473,7 @@ namespace HMAC_bench PICOBENCH(openssl_hmac_sha256_64).PICO_HASH_SUFFIX(); } -std::vector shares; +std::vector shares; PICOBENCH_SUITE("share"); namespace SHARE_bench @@ -488,8 +487,8 @@ namespace SHARE_bench for (auto _ : s) { (void)_; - crypto::Share secret; - crypto::sample_secret_and_shares(secret, shares, threshold); + crypto::sharing::Share secret; + crypto::sharing::sample_secret_and_shares(secret, shares, threshold); do_not_optimize(secret); clobber_memory(); } @@ -521,9 +520,10 @@ namespace SHARE_bench for (auto _ : s) { (void)_; - crypto::Share secret; - crypto::sample_secret_and_shares(secret, shares, threshold); - crypto::recover_unauthenticated_secret(secret, shares, threshold); + crypto::sharing::Share secret; + crypto::sharing::sample_secret_and_shares(secret, shares, threshold); + crypto::sharing::recover_unauthenticated_secret( + secret, shares, threshold); do_not_optimize(secret); clobber_memory(); } diff --git a/src/crypto/test/crypto.cpp b/src/crypto/test/crypto.cpp index c37e46ac1777..cf01aba31df8 100644 --- a/src/crypto/test/crypto.cpp +++ b/src/crypto/test/crypto.cpp @@ -373,7 +373,7 @@ TEST_CASE("base64url") TEST_CASE("Wrap, unwrap with RSAKeyPair") { size_t input_len = 64; - std::vector input = create_entropy()->random(input_len); + std::vector input = get_entropy()->random(input_len); INFO("Cannot make RSA key from EC key"); { @@ -612,7 +612,7 @@ TEST_CASE("AES Key wrap with padding") auto key = get_raw_key(); std::vector aad(123, 'y'); - std::vector key_to_wrap = create_entropy()->random(997); + std::vector key_to_wrap = get_entropy()->random(997); auto ossl = std::make_unique(key); @@ -644,7 +644,7 @@ TEST_CASE("CKM_RSA_PKCS_OAEP") TEST_CASE("CKM_RSA_AES_KEY_WRAP") { - std::vector key_to_wrap = create_entropy()->random(256); + std::vector key_to_wrap = get_entropy()->random(256); auto rsa_kp = make_rsa_key_pair(); auto rsa_pk = make_rsa_public_key(rsa_kp->public_key_pem()); @@ -658,7 +658,7 @@ TEST_CASE("CKM_RSA_AES_KEY_WRAP") TEST_CASE("AES-GCM convenience functions") { - EntropyPtr entropy = create_entropy(); + EntropyPtr entropy = get_entropy(); std::vector key = entropy->random(GCM_DEFAULT_KEY_SIZE); auto encrypted = aes_gcm_encrypt(key, contents); auto decrypted = aes_gcm_decrypt(key, encrypted); diff --git a/src/crypto/test/secret_sharing.cpp b/src/crypto/test/secret_sharing.cpp index 4a9f1a04fd15..43132d3633a2 100644 --- a/src/crypto/test/secret_sharing.cpp +++ b/src/crypto/test/secret_sharing.cpp @@ -10,7 +10,17 @@ #include -using namespace crypto; +using namespace crypto::sharing; + +void check_share_is_not_trivially_wrong(const Share& share) +{ + REQUIRE(share.x != 0); + for (size_t i = 0; i < LIMBS; ++i) + { + REQUIRE(share.y[i] != 0); + REQUIRE(share.y[i] != 0xFFFFFFFF); + } +} void share_and_recover(size_t num_shares, size_t threshold, size_t recoveries) { @@ -19,6 +29,11 @@ void share_and_recover(size_t num_shares, size_t threshold, size_t recoveries) Share secret; sample_secret_and_shares(secret, shares, threshold); + for (const auto& share : shares) + { + check_share_is_not_trivially_wrong(share); + } + std::mt19937 rng{std::random_device{}()}; for (size_t i = 0; i < recoveries; ++i) @@ -129,4 +144,26 @@ TEST_CASE("Serialisation") INFO(new_share.to_str()); REQUIRE(share == new_share); +} + +constexpr element prime = (1ul << 31) - 1ul; // a notorious Mersenne prime +static element reduce(element x) +{ + // Actually CT, as compiled by Clang 11+, but obviously not guaranteed to be + // so + return (x % prime); +} + +TEST_CASE("Smoke test ct_reduce against reduce") +{ + for (size_t i = 0; i < (1ul << 16); ++i) + { + size_t under = prime * i - 1; + size_t over = prime * i; + size_t mid = prime * i + (prime / 2); + + REQUIRE_MESSAGE(reduce(under) == ct_reduce(under), std::to_string(under)); + REQUIRE_MESSAGE(reduce(over) == ct_reduce(over), std::to_string(over)); + REQUIRE_MESSAGE(reduce(mid) == ct_reduce(mid), std::to_string(mid)); + } } \ No newline at end of file diff --git a/src/indexing/enclave_lfs_access.h b/src/indexing/enclave_lfs_access.h index ad78af042181..d7e18200f5f9 100644 --- a/src/indexing/enclave_lfs_access.h +++ b/src/indexing/enclave_lfs_access.h @@ -123,7 +123,7 @@ namespace ccf::indexing public: EnclaveLFSAccess(const ringbuffer::WriterPtr& writer) : to_host(writer), - entropy_src(crypto::create_entropy()) + entropy_src(crypto::get_entropy()) { // Generate a fresh random key. Only this specific instance, in this // enclave, can read these files! diff --git a/src/js/crypto.cpp b/src/js/crypto.cpp index a7192c61fdd9..fdda91bfcb7d 100644 --- a/src/js/crypto.cpp +++ b/src/js/crypto.cpp @@ -35,7 +35,7 @@ namespace ccf::js try { - std::vector key = crypto::create_entropy()->random(key_size / 8); + std::vector key = crypto::get_entropy()->random(key_size / 8); return JS_NewArrayBufferCopy(ctx, key.data(), key.size()); } catch (const std::exception& exc) diff --git a/src/js/wrap.cpp b/src/js/wrap.cpp index 552a3ea7a2f5..c0130c73171b 100644 --- a/src/js/wrap.cpp +++ b/src/js/wrap.cpp @@ -2169,7 +2169,7 @@ namespace ccf::js static JSValue js_random_impl( JSContext* ctx, JSValueConst this_val, int argc, JSValueConst* argv) { - crypto::EntropyPtr entropy = crypto::create_entropy(); + crypto::EntropyPtr entropy = crypto::get_entropy(); // Generate a random 64 bit unsigned int, and transform that to a double // between 0 and 1. Note this is non-uniform, and not cryptographically diff --git a/src/kv/kv_types.h b/src/kv/kv_types.h index a39e2d5fc078..c9bf986538dc 100644 --- a/src/kv/kv_types.h +++ b/src/kv/kv_types.h @@ -476,7 +476,9 @@ namespace kv virtual void enable_all_domains() {} - virtual void set_retired_committed(ccf::SeqNo){}; + virtual void set_retired_committed( + ccf::SeqNo, const std::vector& node_ids) + {} }; struct PendingTxInfo diff --git a/src/node/channels.h b/src/node/channels.h index 06ca979d6c78..76968bd62b06 100644 --- a/src/node/channels.h +++ b/src/node/channels.h @@ -832,7 +832,7 @@ namespace ccf peer_cert = {}; peer_cv.reset(); - auto e = crypto::create_entropy(); + auto e = crypto::get_entropy(); hkdf_salt = e->random(salt_len); // As a future simplification, we would like this to always be true @@ -855,7 +855,7 @@ namespace ccf peer_cert = {}; peer_cv.reset(); - auto e = crypto::create_entropy(); + auto e = crypto::get_entropy(); hkdf_salt = e->random(salt_len); } @@ -973,7 +973,7 @@ namespace ccf status(fmt::format("Channel to {}", peer_id_), INACTIVE), message_limit(message_limit_) { - auto e = crypto::create_entropy(); + auto e = crypto::get_entropy(); hkdf_salt = e->random(salt_len); } diff --git a/src/node/ledger_secret.h b/src/node/ledger_secret.h index ee6de3e4c915..9cecd05d21d9 100644 --- a/src/node/ledger_secret.h +++ b/src/node/ledger_secret.h @@ -76,7 +76,7 @@ namespace ccf inline LedgerSecretPtr make_ledger_secret() { return std::make_shared( - crypto::create_entropy()->random(crypto::GCM_DEFAULT_KEY_SIZE)); + crypto::get_entropy()->random(crypto::GCM_DEFAULT_KEY_SIZE)); } inline std::vector decrypt_previous_ledger_secret_raw( diff --git a/src/node/node_state.h b/src/node/node_state.h index ec8407d77936..6be6c443e43a 100644 --- a/src/node/node_state.h +++ b/src/node/node_state.h @@ -2148,23 +2148,16 @@ namespace ccf network.nodes.get_name(), network.nodes.wrap_commit_hook( [this](kv::Version hook_version, const Nodes::Write& w) { + std::vector retired_committed_nodes; for (const auto& [node_id, node_info] : w) { - if (node_id != self) + if (node_info.has_value() && node_info->retired_committed) { - // Only update our own state - continue; - } - - if (node_info.has_value()) - { - if (node_info->retired_committed) - { - consensus->set_retired_committed(hook_version); - } - return; + retired_committed_nodes.push_back(node_id); } } + consensus->set_retired_committed( + hook_version, retired_committed_nodes); })); // Service-endorsed certificate is passed to history as early as _local_ diff --git a/src/node/secret_share.h b/src/node/secret_share.h index 0fac33e6cb1b..e8939e2679b6 100644 --- a/src/node/secret_share.h +++ b/src/node/secret_share.h @@ -17,7 +17,7 @@ extern "C" /// SSS assumes that there is a function of this prototype int randombytes(void* buf, size_t n) { - crypto::EntropyPtr entropy = crypto::create_entropy(); + crypto::EntropyPtr entropy = crypto::get_entropy(); entropy->random((unsigned char*)buf, n); return 0; } diff --git a/src/node/share_manager.h b/src/node/share_manager.h index 5c5747e83a1e..45d071dd6c1a 100644 --- a/src/node/share_manager.h +++ b/src/node/share_manager.h @@ -27,7 +27,7 @@ namespace ccf size_t num_shares; size_t recovery_threshold; std::vector data; // Referred to as "kz" in TR - std::vector shares; + std::vector shares; public: LedgerSecretWrappingKey(size_t num_shares_, size_t recovery_threshold_) : @@ -35,18 +35,20 @@ namespace ccf recovery_threshold(recovery_threshold_) { shares.resize(num_shares); - crypto::Share secret; - sample_secret_and_shares(secret, shares, recovery_threshold); + crypto::sharing::Share secret; + crypto::sharing::sample_secret_and_shares( + secret, shares, recovery_threshold); data = secret.key(KZ_KEY_SIZE); } LedgerSecretWrappingKey( - std::vector&& shares_, size_t recovery_threshold_) : + std::vector&& shares_, + size_t recovery_threshold_) : recovery_threshold(recovery_threshold_) { shares = shares_; - crypto::Share secret; - crypto::recover_unauthenticated_secret( + crypto::sharing::Share secret; + crypto::sharing::recover_unauthenticated_secret( secret, shares, recovery_threshold); data = secret.key(KZ_KEY_SIZE); } @@ -79,7 +81,7 @@ namespace ccf std::vector> get_shares() const { std::vector> shares_; - for (const crypto::Share& share : shares) + for (const crypto::sharing::Share& share : shares) { shares_.emplace_back(share.serialise()); } @@ -314,7 +316,7 @@ namespace ccf Tables::ENCRYPTED_SUBMITTED_SHARES); auto config = tx.rw(Tables::CONFIGURATION); - std::vector new_shares = {}; + std::vector new_shares = {}; std::vector old_shares = {}; // Defensively allow shares in both formats for the time being, even if we // get a mix, and so long as we have enough of one or the other, attempt @@ -328,7 +330,7 @@ namespace ccf encrypted_share, ledger_secrets->get_latest(tx).second); switch (decrypted_share.size()) { - case crypto::Share::serialised_size: + case crypto::sharing::Share::serialised_size: { new_shares.emplace_back(decrypted_share); break; @@ -351,7 +353,7 @@ namespace ccf "is neither a new-style share of {} bytes nor an old-style " "share of {} bytes", decrypted_share.size(), - crypto::Share::serialised_size, + crypto::sharing::Share::serialised_size, SecretSharing::SHARE_LENGTH)); } } diff --git a/src/node/test/secret_share.cpp b/src/node/test/secret_share.cpp index d9febf14e099..ed9faf672088 100644 --- a/src/node/test/secret_share.cpp +++ b/src/node/test/secret_share.cpp @@ -15,8 +15,8 @@ TEST_CASE("Simple test") INFO("Data to split must be have fixed length"); { - auto random = crypto::create_entropy()->random( - ccf::SecretSharing::SECRET_TO_SPLIT_LENGTH); + auto random = + crypto::get_entropy()->random(ccf::SecretSharing::SECRET_TO_SPLIT_LENGTH); std::copy_n( random.begin(), ccf::SecretSharing::SECRET_TO_SPLIT_LENGTH, diff --git a/tla/consensus/MCAliases.tla b/tla/consensus/MCAliases.tla index d9a2e4389872..2be42c55db37 100644 --- a/tla/consensus/MCAliases.tla +++ b/tla/consensus/MCAliases.tla @@ -69,6 +69,7 @@ DebugAliasVars == messages |-> messages, currentTerm |-> currentTerm, leadershipState |-> leadershipState, + membershipState |-> membershipState, votedFor |-> votedFor, \* More compact visualization of the log. \* lg |-> [ s \in Servers |-> StringifyLog(s) ], diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg index b94a6beb3d7f..afbec1250359 100644 --- a/tla/consensus/MCccfraft.cfg +++ b/tla/consensus/MCccfraft.cfg @@ -43,6 +43,7 @@ CONSTANTS TypeEntry = Entry TypeSignature = Signature TypeReconfiguration = Reconfiguration + TypeRetiredCommitted = RetiredCommitted NodeOne = n1 NodeTwo = n2 @@ -83,3 +84,5 @@ INVARIANTS LogConfigurationConsistentInv MembershipStateConsistentInv CommitCommittableIndices + ReplicationInv + RetiredCommittedInv diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg index 39a9cb9a2e42..3801e38048d9 100644 --- a/tla/consensus/MCccfraftAtomicReconfig.cfg +++ b/tla/consensus/MCccfraftAtomicReconfig.cfg @@ -43,6 +43,7 @@ CONSTANTS TypeEntry = Entry TypeSignature = Signature TypeReconfiguration = Reconfiguration + TypeRetiredCommitted = RetiredCommitted NodeOne = n1 NodeTwo = n2 @@ -82,4 +83,6 @@ INVARIANTS LogConfigurationConsistentInv MembershipStateConsistentInv NoLeaderBeforeInitialTerm - CommitCommittableIndices \ No newline at end of file + CommitCommittableIndices + ReplicationInv + RetiredCommittedInv diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg index 08aee6cdc773..c9471765cb6b 100644 --- a/tla/consensus/MCccfraftWithReconfig.cfg +++ b/tla/consensus/MCccfraftWithReconfig.cfg @@ -43,6 +43,7 @@ CONSTANTS TypeEntry = Entry TypeSignature = Signature TypeReconfiguration = Reconfiguration + TypeRetiredCommitted = RetiredCommitted NodeOne = n1 NodeTwo = n2 @@ -83,3 +84,5 @@ INVARIANTS LogConfigurationConsistentInv MembershipStateConsistentInv CommitCommittableIndices + ReplicationInv + RetiredCommittedInv diff --git a/tla/consensus/SIMCoverageccfraft.cfg b/tla/consensus/SIMCoverageccfraft.cfg index 01bae688c635..5ef717fb59b3 100644 --- a/tla/consensus/SIMCoverageccfraft.cfg +++ b/tla/consensus/SIMCoverageccfraft.cfg @@ -30,6 +30,7 @@ CONSTANTS TypeEntry = Entry TypeSignature = Signature TypeReconfiguration = Reconfiguration + TypeRetiredCommitted = RetiredCommitted NodeOne = n1 NodeTwo = n2 diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg index 3d46f2c75d60..3ea532e84d10 100644 --- a/tla/consensus/SIMccfraft.cfg +++ b/tla/consensus/SIMccfraft.cfg @@ -30,6 +30,7 @@ CONSTANTS TypeEntry = Entry TypeSignature = Signature TypeReconfiguration = Reconfiguration + TypeRetiredCommitted = RetiredCommitted NodeOne = n1 NodeTwo = n2 @@ -96,6 +97,9 @@ INVARIANTS CommitCommittableIndices + ReplicationInv + RetiredCommittedInv + \* DebugInvLeaderCannotStepDown \* DebugInvAnyCommitted \* DebugInvAllCommitted diff --git a/tla/consensus/Traceccfraft.cfg b/tla/consensus/Traceccfraft.cfg index 3c0b7b98f73d..f74cec141316 100644 --- a/tla/consensus/Traceccfraft.cfg +++ b/tla/consensus/Traceccfraft.cfg @@ -82,6 +82,7 @@ CONSTANTS TypeEntry = TypeEntry TypeSignature = TypeSignature TypeReconfiguration = TypeReconfiguration + TypeRetiredCommitted = RetiredCommitted \* state.h my_node_id is a string. NodeOne = "0" diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla index 0b3c8cc6810b..1b69b4cb7d8e 100644 --- a/tla/consensus/Traceccfraft.tla +++ b/tla/consensus/Traceccfraft.tla @@ -7,8 +7,16 @@ RaftMsgType == "raft_request_vote" :> RequestVoteRequest @@ "raft_request_vote_response" :> RequestVoteResponse @@ "raft_propose_request_vote" :> ProposeVoteRequest -LeadershipState == - Leader :> "Leader" @@ Follower :> "Follower" @@ Candidate :> "Candidate" @@ None :> "None" +ToLeadershipState == + "Leader" :> Leader @@ + "Follower" :> Follower @@ + "Candidate" :> Candidate @@ + "None" :> None + +ToMembershipState == + \* https://github.com/microsoft/CCF/blob/61bc8ef25ba636b6f5915dfc69647e2ae9cf47c7/tla/consensus/ccfraft.tla#L54 + "Active" :> {Active} @@ + "Retired" :> {RetirementOrdered, RetirementSigned, RetirementCompleted} IsAppendEntriesRequest(msg, dst, src, logline) == (* @@ -147,12 +155,20 @@ IsTimeout == /\ logline.msg.state.leadership_state = "Candidate" /\ Timeout(logline.msg.state.node_id) /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx IsBecomeLeader == /\ IsEvent("become_leader") /\ logline.msg.state.leadership_state = "Leader" /\ BecomeLeader(logline.msg.state.node_id) /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx IsClientRequest == /\ IsEvent("replicate") @@ -161,6 +177,10 @@ IsClientRequest == \* TODO Consider creating a mapping from clientRequests to actual values in the system trace. \* TODO Alternatively, extract the written values from the system trace and redefine clientRequests at startup. /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx IsSendAppendEntries == /\ IsEvent("send_append_entries") @@ -179,6 +199,10 @@ IsSendAppendEntries == \* /\ logline.msg.sent_idx = nextIndex[i][j] /\ logline.msg.match_idx = matchIndex[i][j] /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx IsRcvAppendEntriesRequest == /\ IsEvent("recv_append_entries") @@ -192,6 +216,10 @@ IsRcvAppendEntriesRequest == \* HandleAppendEntriesRequest step that leaves messages unchanged. \/ RAERRAER(m):: (UNCHANGED messages /\ HandleAppendEntriesRequest(i, j, m)) \cdot HandleAppendEntriesRequest(i, j, m) /\ IsAppendEntriesRequest(m, i, j, logline) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + \* TODO /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx IsSendAppendEntriesResponse == \* Skip saer because ccfraft!HandleAppendEntriesRequest atomcially handles the request and sends the response. @@ -199,6 +227,10 @@ IsSendAppendEntriesResponse == /\ IsEvent("send_append_entries_response") /\ UNCHANGED vars /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx IsAddConfiguration == /\ IsEvent("add_configuration") @@ -208,6 +240,10 @@ IsAddConfiguration == \* recv_append_entries will update the committable indices in the spec, but not in the impl state, which then goes on to handle an \* add_configuration event on which state->committable_indices is (correctly) empty. \* /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + \* TODO: /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + \*TODO /\ membershipState'[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx IsSignCommittableMessages == /\ IsEvent("replicate") @@ -220,6 +256,10 @@ IsSignCommittableMessages == \* the subsequent send_append_entries will assert the effect of SignCommittableMessages anyway. \* Also see IsExecuteAppendEntries below. /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx IsAdvanceCommitIndex == \* This is enabled *after* a SignCommittableMessages because ACI looks for a @@ -230,9 +270,17 @@ IsAdvanceCommitIndex == IN /\ AdvanceCommitIndex(i) /\ commitIndex'[i] = logline.msg.args.idx /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx \/ /\ IsEvent("commit") /\ UNCHANGED vars /\ logline.msg.state.leadership_state = "Follower" + \* TODO: /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx IsChangeConfiguration == /\ IsEvent("add_configuration") @@ -241,6 +289,10 @@ IsChangeConfiguration == newConfiguration == DOMAIN logline.msg.args.configuration.nodes IN ChangeConfigurationInt(i, newConfiguration) /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx IsRcvAppendEntriesResponse == /\ IsEvent("recv_append_entries_response") @@ -259,6 +311,10 @@ IsRcvAppendEntriesResponse == /\ DropStaleResponse(i, j, m) /\ IsAppendEntriesResponse(m, i, j, logline) /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + \*TODO /\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx IsSendRequestVote == /\ IsEvent("send_request_vote") @@ -274,6 +330,10 @@ IsSendRequestVote == \* There is now one more message of this type. /\ Network!OneMoreMessage(m) /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx IsRcvRequestVoteRequest == \/ /\ IsEvent("recv_request_vote") @@ -292,6 +352,10 @@ IsRcvRequestVoteRequest == \* (see https://github.com/microsoft/CCF/issues/5057#issuecomment-1487279316) \/ UpdateTerm(i, j, m) \cdot HandleRequestVoteRequest(i, j, m) /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + \*TODO/\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx IsExecuteAppendEntries == \* Skip append because ccfraft!HandleRequestVoteRequest atomcially handles the request, sends the response, @@ -302,6 +366,10 @@ IsExecuteAppendEntries == /\ UNCHANGED vars /\ leadershipState[logline.msg.state.node_id] = Follower /\ currentTerm[logline.msg.state.node_id] = logline.msg.state.current_view + \* TODO: /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx IsRcvRequestVoteResponse == /\ IsEvent("recv_request_vote_response") @@ -318,18 +386,30 @@ IsRcvRequestVoteResponse == \/ UpdateTerm(i, j, m) \cdot DropResponseWhenNotInState(i, j, m) \/ DropResponseWhenNotInState(i, j, m) /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + \*TODO/\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx IsBecomeFollower == /\ IsEvent("become_follower") /\ UNCHANGED vars \* UNCHANGED implies that it doesn't matter if we prime the previous variables. /\ leadershipState[logline.msg.state.node_id] # Leader /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx IsCheckQuorum == /\ IsEvent("become_follower") /\ CheckQuorum(logline.msg.state.node_id) /\ leadershipState[logline.msg.state.node_id] = Leader /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx IsRcvProposeVoteRequest == /\ IsEvent("recv_propose_request_vote") @@ -340,6 +420,10 @@ IsRcvProposeVoteRequest == /\ m.term = logline.msg.packet.term /\ UNCHANGED vars /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id) + /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx + /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state] + /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state] + /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx TraceNext == \/ IsTimeout diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index a1634459e5f3..3f7ba6daf9a7 100644 --- a/tla/consensus/ccfraft.tla +++ b/tla/consensus/ccfraft.tla @@ -91,7 +91,8 @@ CONSTANTS CONSTANTS TypeEntry, TypeSignature, - TypeReconfiguration + TypeReconfiguration, + TypeRetiredCommitted \* Set of nodes for this model CONSTANTS Servers @@ -165,6 +166,8 @@ EntryTypeOK(entry) == \/ entry.contentType = TypeSignature \/ /\ entry.contentType = TypeReconfiguration /\ entry.configuration \subseteq Servers + \/ /\ entry.contentType = TypeRetiredCommitted + /\ entry.retired \subseteq Servers AppendEntriesRequestTypeOK(m) == /\ m.type = AppendEntriesRequest @@ -515,6 +518,14 @@ CalcMembershipState(log_i, commit_index_i, i) == ELSE RetirementOrdered ELSE Active +\* Set of nodes with retired committed transactions in a given log +AllRetiredCommittedTxns(log_i) == + UNION {log_i[idx].retired: idx \in {k \in DOMAIN log_i: log_i[k].contentType = TypeRetiredCommitted}} + +\* Set of retired nodes in a given log +AllRetired(log_i) == + {n \in Servers: RetirementIndexLog(log_i, n) # 0} + AppendEntriesBatchsize(i, j) == \* The Leader is modeled to send zero to one entries per AppendEntriesRequest. \* This can be redefined to send bigger batches of entries. @@ -687,6 +698,7 @@ BecomeLeader(i) == \* been rolled back as it was unsigned /\ membershipState' = [membershipState EXCEPT ![i] = IF @ = RetirementOrdered THEN Active ELSE @] + \* TODO: Check if any node's retirement has been committed and add retired_committed if so /\ UNCHANGED <> \* Leader i receives a client request to add 42 to the log. @@ -765,6 +777,20 @@ ChangeConfiguration(i) == \E newConfiguration \in SUBSET(Servers) \ {{}}: ChangeConfigurationInt(i, newConfiguration) +RetiredCommitted(i) == + /\ leadershipState[i] = Leader + /\ LET + \* Calculate which nodes have had their retirement committed but no retired committed txn + retire_committed_nodes == AllRetired(SubSeq(log[i],1,commitIndex[i])) \ AllRetiredCommittedTxns(log[i]) + IN + /\ retire_committed_nodes # {} + /\ log' = [log EXCEPT ![i] = Append(@, [ + term |-> currentTerm[i], + contentType |-> TypeRetiredCommitted, + retired |-> retire_committed_nodes])] + /\ UNCHANGED <> + + \* Leader i advances its commitIndex to the next possible Index. \* This is done as a separate step from handling AppendEntries responses, \* in part to minimize atomic regions, and in part so that leaders of @@ -831,7 +857,7 @@ AdvanceCommitIndex(i) == ELSE UNCHANGED <> \* Otherwise, Configuration and states remain unchanged ELSE UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> \* CCF supports checkQuorum which enables a leader to choose to abdicate leadership. CheckQuorum(i) == @@ -1205,6 +1231,7 @@ NextInt(i) == \/ ClientRequest(i) \/ SignCommittableMessages(i) \/ ChangeConfiguration(i) + \/ RetiredCommitted(i) \/ AdvanceCommitIndex(i) \/ CheckQuorum(i) \/ \E j \in Servers : RequestVote(i, j) @@ -1425,6 +1452,49 @@ CommitCommittableIndices == /\ CommittableIndices(i) = {} \/ commitIndex[i] \in CommittableIndices(i) + +\* Given a committed log log_x for some node and an index idx into that log, +\* GetConfigurations returns all configurations which should have replicated +\* the transaction at idx. +GetConfigurations(log_x, idx) == + LET + configs_all == {k \in DOMAIN log_x : log_x[k].contentType = TypeReconfiguration} + configs_before == {k \in configs_all : k <= idx} + \* This if-statement should not be needed as genesis transaction should be a configuration + config_last == IF configs_before = {} THEN {} ELSE {Max(configs_before)} + configs_after == {k \in configs_all : k > idx} + IN + {log_x[i].configuration : i \in (configs_after \union config_last)} + +\* ReplicationInv states that all log entries that are believed to be committed must be +\* replicated on a quorum of nodes from the preceding configuration and all subsequent +\* committed configurations. +ReplicationInv == + \E i \in Servers : + \* We just check the node with the highest commitIndex + \* LogInv ensures that includes all committed transactions + /\ \A j \in Servers: commitIndex[i] >= commitIndex[j] + \* Every committed transaction must be replicated to at least + \* one quorum in each configuration which should have a copy + /\ \A idx \in DOMAIN Committed(i) : + \A config \in GetConfigurations(Committed(i), idx) : + \E quorum \in Quorums[config] : + \A node \in quorum : + /\ Len(log[node]) >= idx + /\ log[node][idx] = log[i][idx] + + + +\* Check that retired committed transactions are added only when retirement committed has been observed +RetiredCommittedInv == + \A i \in Servers : + \A k \in DOMAIN log[i] : + log[i][k].contentType = TypeRetiredCommitted + => \A j \in log[i][k].retired : + /\ RetirementIndexLog(log[i],j) # 0 + /\ RetirementIndexLog(log[i],j) <= k + /\ RetirementIndexLog(log[i],j) <= commitIndex[i] + ------------------------------------------------------------------------------ \* Properties diff --git a/tla/last_line.sh b/tla/last_line.sh new file mode 100755 index 000000000000..82487864c36f --- /dev/null +++ b/tla/last_line.sh @@ -0,0 +1,16 @@ +#!/bin/bash +# Copyright (c) Microsoft Corporation. All rights reserved. +# Licensed under the Apache 2.0 License. + +# Extract a summary of the last line in a trace, useful when finding out where a scenario has mismatched + +RED="\033[31m" +NORMAL="\033[0;39m" + +if [ -e "$1" ]; then + echo -ne "$RED" + cat "$1" | jq '.action | last | .[2][1]._logline | "Last matched [" + .h_ts + "] " + .msg.function + " (" + .cmd + ")"' | xargs + echo -ne "$NORMAL" + exit 1 +fi +exit 0 \ No newline at end of file diff --git a/tla/tlc.sh b/tla/tlc.sh index bcc14c3fd009..1fe2ee90d2d0 100755 --- a/tla/tlc.sh +++ b/tla/tlc.sh @@ -4,13 +4,17 @@ # Original License below # Adapted from: https://github.com/pmer/tla-bin -TLC_OPTIONS=() - if [ "${CI}" ] || [ "${SYSTEM_TEAMFOUNDATIONCOLLECTIONURI}" ]; then - JVM_OPTIONS=("-Dtlc2.TLC.ide=Github" "-Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601") + JVM_OPTIONS+=("-Dtlc2.TLC.ide=Github" "-Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601") fi -exec java -XX:+UseParallelGC -Dtlc2.tool.impl.Tool.cdot=true "${JVM_OPTIONS[@]}" -cp tla2tools.jar:CommunityModules-deps.jar tlc2.TLC "$@" -lncheck final "${TLC_OPTIONS[@]}" +# See https://docs.oracle.com/en/java/javase/20/gctuning/available-collectors.html#GUID-F215A508-9E58-40B4-90A5-74E29BF3BD3C +# > If (a) peak application performance is the first priority and (b) there are no pause-time requirements or pauses of one second or longer are acceptable, +# > then let the VM select the collector or select the parallel collector with -XX:+UseParallelGC. +# Simulation, nor Model Checking seem to work well with G1GC, but Trace Validation does not for some reason, and is much slower unless -XX:+UseParallelGC is used. +# In all cases, pauses don't matter, only throughput does. + +exec java -XX:+UseParallelGC -Dtlc2.tool.impl.Tool.cdot=true "${JVM_OPTIONS[@]}" -cp tla2tools.jar:CommunityModules-deps.jar tlc2.TLC "$@" -checkpoint 0 -lncheck final # Original License