diff --git a/.claude/skills/add-verified-component/SKILL.md b/.claude/skills/add-verified-component/SKILL.md new file mode 100644 index 0000000000..ae88c5e1fa --- /dev/null +++ b/.claude/skills/add-verified-component/SKILL.md @@ -0,0 +1,286 @@ +--- +name: add-verified-component +description: Add a new formally verified F*/Pulse component to the collector's verified library — replaces C++ internals with extracted verified C code +--- + +# Add Verified Component + +Replace C++ component internals with a formally verified implementation written in F*/Pulse, extracted to C via Karamel. The verified code proves both memory safety and functional correctness. The C++ class becomes a thin wrapper around the extracted C API. + +## Architecture + +Each verified component follows the ghost-spec-as-invariant pattern: + +1. **Spec module** (`XSpec.fst`) — pure functional implementation + correctness lemmas. Marked `[@@noextract_to "krml"]`. Never extracted. Serves as ground truth. +2. **Pulse module** (`XPulse.fst`) — heap implementation using `Pulse.Lib.Box` for allocation. Maintains a ghost invariant linking heap state to the spec. This IS the code that runs. +3. **C++ wrapper** — thin class forwarding to the extracted C API via `extern "C"`. Preserves the existing public API so callers don't change. + +Proofs compose: each component's spec can reference other components' specs. + +## Prerequisites + +- F* 2026.03.24~dev with Pulse: `opam exec -- fstar.exe --version` +- Karamel: `~/code/go/src/github.com/FStarLang/FStar/karamel/krml` +- Collector builder container running: `DOCKER_HOST=unix:///run/podman/podman.sock docker ps | grep collector_builder` + +## Process + +### 1. Analyse the C++ component + +Read the target header and implementation files in `collector/lib/`. Identify: + +- **Operations** to verify (insert, find, delete, etc.) +- **Data types** used — which are value types vs heap-allocated structures +- **Key properties** that should hold (invariants, boundary conditions, correctness) +- **Byte-order concerns** — the collector stores IPv4 addresses in two `uint64_t`s in network byte order on a little-endian machine + +### 2. Write the spec module (XSpec.fst) + +Create `collector/verified/fstar/XSpec.fst` with: + +- Pure functional data types (algebraic types are fine here — they're never extracted) +- Pure functions implementing the algorithm +- Correctness lemmas (use `admit()` initially, discharge later) +- Everything marked `[@@noextract_to "krml"]` EXCEPT pure helper functions that the Pulse module will call directly (those need `inline_for_extraction`) + +```fstar +module XSpec + +[@@noextract_to "krml"] +noeq type my_tree = + | Leaf : my_tree + | Node : value:my_type -> left:my_tree -> right:my_tree -> my_tree + +[@@noextract_to "krml"] +let rec find (tree:my_tree) (key:key_t) : option my_type = ... + +[@@noextract_to "krml"] +let lemma_find_correct (tree:my_tree) (key:key_t) + : Lemma (ensures ...) = admit () // discharge later +``` + +Verify: +```bash +cd collector/verified +opam exec -- fstar.exe --z3rlimit 80 --include fstar fstar/XSpec.fst +``` + +### 3. Write the Pulse module (XPulse.fst) + +Create `collector/verified/fstar/XPulse.fst` with `#lang-pulse`. + +**Key conventions:** + +- Use `Pulse.Lib.Box` for heap-allocated pointers (`box a`, `alloc`, `free`, `!`, `:=`) +- Use `option (box node_t)` for nullable pointers (NOT raw `box` with `is_null` — the option pattern works better with Karamel extraction) +- Define a recursive `slprop` invariant linking heap to ghost spec +- Write ghost helper functions for `fold`/`unfold` of the invariant +- Each operation proves its postcondition matches the spec +- Use `fn rec` with `decreases` for recursive traversals + +```fstar +module XPulse +#lang-pulse + +open Pulse.Lib.Pervasives +module Box = Pulse.Lib.Box +open Pulse.Lib.Box { box, (:=), (!) } +open XSpec + +// Heap node type +noeq type node_t = { + value: my_type; + left: tree_ptr; + right: tree_ptr; +} +and node_box = box node_t +and tree_ptr = option node_box + +// Ghost invariant: links heap to spec +let rec is_tree (ct: tree_ptr) (ft: XSpec.my_tree) + : Tot slprop (decreases ft) = ... + +// Operations with proof obligations +fn find (t: handle) (#ft: erased XSpec.my_tree) (key: key_t) + requires is_tree t.root ft + returns result: find_result + ensures is_tree t.root ft ** + pure (result == XSpec.find (reveal ft) key) +{ ... } +``` + +Verify: +```bash +cd collector/verified +opam exec -- fstar.exe --z3rlimit 80 --include fstar \ + --include /home/ghutton/.opam/default/lib/fstar/pulse \ + fstar/XPulse.fst +``` + +**Important Karamel constraints:** +- Recursive algebraic types (like `noeq type tree = Leaf | Node ...`) cause Karamel to hang. Use `option (box node_t)` instead — Pulse's Box extracts to C malloc/free pointers which Karamel handles. +- Avoid `FStar.Pervasives.Native.option` in types unless you bundle `FStar.Pervasives.Native` in the extraction. +- Use `bool` flags instead of `option` for return types where possible. +- Machine integers only (`U8.t`, `U32.t`, `U64.t`) in extractable code — `nat`/`int` produce `krml_checked_int_t`. + +### 4. Update the Makefile and extract to C + +Add your modules to `collector/verified/Makefile`: + +- Add spec file to `SPEC_FILES` +- Add Pulse module to `MODULES` +- Add explicit `verify-X` and `extract-X` targets + +For the extraction command, include dependent modules in `--extract` and `-bundle`: +```makefile +extract-XPulse: verify-XPulse + $(FSTAR_EXE) $(FSTAR_FLAGS) --codegen krml \ + --extract 'NetworkTypes,XSpec,XPulse,FStar.Pervasives.Native' \ + fstar/XPulse.fst + mv out.krml out_XPulse.krml + rm -f extracted/XPulse.c extracted/XPulse.h extracted/Prims.h extracted/Makefile.include + $(KRML_EXE) $(KRML_BASE_FLAGS) \ + -bundle 'NetworkTypes' \ + -bundle 'XPulse=XPulse,XSpec,FStar.Pervasives.Native' \ + out_XPulse.krml +``` + +Run extraction: +```bash +cd collector/verified && make extract-XPulse +``` + +Check for clean extraction — no `krml_checked_int_t` in the generated `.c`/`.h` files. + +### 5. Add to the verified static library + +Add the new `.c` file to `collector/verified/CMakeLists.txt`: + +```cmake +add_library(verified STATIC + extracted/NetworkTypes.c + extracted/NetworkOps.c + extracted/XPulse.c # new +) +``` + +The library is already linked to `collector_lib` — no other CMake changes needed. + +### 6. Write the C++ wrapper + +Replace the C++ class internals to forward to the extracted C API: + +```cpp +extern "C" { +#include "extracted/XPulse.h" +#include "extracted/NetworkTypes.h" +} + +class MyClass { + XPulse_handle handle_; +public: + MyClass() : handle_(XPulse_create()) {} + ~MyClass() { XPulse_destroy(handle_); } + Result Find(Key k) const { + auto result = XPulse_find(handle_, to_verified(k)); + return from_verified(result); + } +}; +``` + +Conversion functions (`to_verified`/`from_verified`) handle the type boundary. Keep them in an anonymous namespace in the `.cpp` file. + +### 7. Write property tests + +Add a test file in `collector/verified/tests/`. Two categories: + +**Public API tests** — exercise the C++ wrapper to validate integration: +```cpp +check("Find after insert returns containing network", [](IPNet net) { + RC_PRE(!net.IsNull() && net.bits() >= 1u); + MyClass obj; + obj.Insert(net); + auto result = obj.Find(net.address()); + RC_ASSERT(!result.IsNull()); + RC_ASSERT(result.Contains(net.address())); +}); +``` + +**Raw verified API tests** — exercise the extracted C directly: +```cpp +check("Verified: insert then find succeeds", [](IPNet net) { + RC_PRE(!net.IsNull() && net.bits() >= 1u); + auto tree = XPulse_create(); + tree = XPulse_insert(tree, to_verified(net)); + auto result = XPulse_find(tree, to_verified(net.address())); + RC_ASSERT(result.found); + XPulse_destroy(tree); +}); +``` + +Register in `collector/verified/tests/CMakeLists.txt`: +```cmake +add_executable(test_verified_x test_x.cpp) +target_link_libraries(test_verified_x collector_lib verified rapidcheck) +add_test(NAME test_verified_x COMMAND test_verified_x) +``` + +### 8. Build and test + +```bash +# Build everything +make -C collector collector + +# Run all tests +DOCKER_HOST=unix:///run/podman/podman.sock docker exec collector_builder_amd64 \ + ctest -V --test-dir /cmake-build + +# Run just verified tests +DOCKER_HOST=unix:///run/podman/podman.sock docker exec collector_builder_amd64 \ + ctest -V -R test_verified --test-dir /cmake-build +``` + +All existing tests must pass unchanged — the public API is preserved. + +### 9. Discharge admitted proofs + +Go back and replace `admit()` in spec lemmas with actual proofs. Work iteratively — verify after each lemma. + +## Existing verified components + +| Component | Spec | Pulse | C++ Wrapper | Properties | +|-----------|------|-------|-------------|------------| +| NetworkConnection | NetworkTypes.fst | — (pure functions only) | — (differential tests) | IsLocal, IsPublic, IsEphemeralPort, IsCanonicalExternal, CIDR containment | +| NRadix tree | NRadixSpec.fst | NRadixPulse.fst | NRadix.h/cpp | create, destroy, insert (with duplicate detection), find, is_empty. Ghost invariant links heap tree to functional spec. | + +## File layout + +``` +collector/verified/ + .gitignore — Ignores .checked and .krml files + CMakeLists.txt — Builds libverified.a static library + Makefile — F* verify + Karamel extract pipeline + fstar/ + NetworkTypes.fst — Address, IPNet, Endpoint types (shared) + NetworkOps.fst — Classification functions (pure) + NRadixSpec.fst — Functional tree spec + correctness lemmas (not extracted) + NRadixPulse.fst — Pulse heap tree implementation (extracted) + extracted/ + krml_compat.h — Standard includes + KRML macros (hand-written, stable) + NetworkTypes.c/h — Shared type definitions (generated) + NetworkOps.c/h — Classification functions (generated) + NRadixPulse.c/h — Heap tree operations (generated) + tests/ + CMakeLists.txt — Test targets, links collector_lib + verified + rapidcheck + test_network.cpp — Property tests for NetworkOps + test_nradix.cpp — Property tests for NRadix tree +``` + +## Lessons learned + +- **Karamel cannot extract recursive algebraic types** (its inlining phase hangs). Use `option (box node_t)` for tree structures — Pulse's Box extracts to C pointers which Karamel handles. +- **Pulse's `option (box _)` pattern** is the idiomatic way to model nullable pointers (used by Pulse.Lib.LinkedList and Pulse.Lib.AVLTree). +- **Ghost helpers are essential.** Write `intro_`/`elim_` ghost functions for fold/unfold of the recursive `slprop` invariant. Every operation needs them. +- **Use `fn rec` with `decreases`** for recursive traversals. Decrease on the ghost spec tree for read-only operations, on a counter for mutating operations. +- **`remove_definitions()` in CMakeLists.txt** — the parent CMake scope may have `add_definitions` with problematic values (e.g. commas). Use `remove_definitions()` to isolate the verified library. +- **Name verified modules to avoid header clashes** — e.g. `NRadixPulse.h` not `NRadix.h` (which is the C++ header). Include with `extracted/` prefix for clarity. diff --git a/collector/CMakeLists.txt b/collector/CMakeLists.txt index 2d0a6a2152..af0b717a79 100644 --- a/collector/CMakeLists.txt +++ b/collector/CMakeLists.txt @@ -70,6 +70,7 @@ add_definitions(-DSCAP_SOCKET_ONLY_FD) add_definitions("-DINTERESTING_SUBSYS=\"perf_event\", \"cpu\", \"cpuset\", \"memory\"") add_subdirectory(lib) +add_subdirectory(verified) add_executable(collector collector.cpp) target_link_libraries(collector collector_lib) @@ -80,6 +81,7 @@ target_link_libraries(connscrape collector_lib) add_executable(self-checks self-checks.cpp) add_subdirectory(test) +add_subdirectory(verified/tests) # Falco Wrapper Library set(BUILD_DRIVER OFF CACHE BOOL "Build the driver on Linux" FORCE) diff --git a/collector/Makefile b/collector/Makefile index 1e9fa42fe4..c4aa935200 100644 --- a/collector/Makefile +++ b/collector/Makefile @@ -59,6 +59,10 @@ unittest: collector docker exec $(COLLECTOR_BUILDER_NAME) \ ctest --no-tests=error -V --test-dir $(CMAKE_DIR) +verified-tests: collector + docker exec $(COLLECTOR_BUILDER_NAME) \ + ctest --no-tests=error -V -R test_verified --test-dir $(CMAKE_DIR) + .PHONY: txt-files txt-files: mkdir -p container/THIRD_PARTY_NOTICES/ diff --git a/collector/lib/CMakeLists.txt b/collector/lib/CMakeLists.txt index 1d5386e7d1..75ccfd3f0e 100644 --- a/collector/lib/CMakeLists.txt +++ b/collector/lib/CMakeLists.txt @@ -38,3 +38,4 @@ if (COVERAGE) endif() target_link_libraries(collector_lib z ssl crypto bpf) +target_link_libraries(collector_lib verified) diff --git a/collector/lib/NRadix.cpp b/collector/lib/NRadix.cpp index 911be3b140..ba19f209e8 100644 --- a/collector/lib/NRadix.cpp +++ b/collector/lib/NRadix.cpp @@ -1,29 +1,7 @@ -/* Based on src/core/ngx_radix_tree.c from NGINX +/* NRadix.cpp - Radix tree for IP network lookup. * - * Copyright (C) 2002-2021 Igor Sysoev - * Copyright (C) 2011-2021 Nginx, Inc. - * All rights reserved. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions - * are met: - * 1. Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * 2. Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in the - * documentation and/or other materials provided with the distribution. - * - * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND - * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE - * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL - * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS - * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) - * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT - * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY - * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF - * SUCH DAMAGE. + * Backed by a formally verified Pulse/F* implementation. + * This file provides C++ wrappers that forward to the verified C API. */ #include "NRadix.h" @@ -32,97 +10,100 @@ namespace collector { -bool NRadixTree::Insert(const IPNet& network) const { - if (network.IsNull()) { - CLOG(ERROR) << "Cannot handle null IP networks in network tree"; - return false; - } +namespace { - if (network.bits() < 1 || network.bits() > 128) { - CLOG(ERROR) << "Cannot handle CIDR " << network << " with /" << network.bits() << " , in network tree"; - return false; +NetworkTypes_address to_verified_addr(const Address& addr) { + NetworkTypes_address va; + va.hi = addr.array()[0]; + va.lo = addr.array()[1]; + switch (addr.family()) { + case Address::Family::IPV4: + va.family = NetworkTypes_FamilyIPv4; + break; + case Address::Family::IPV6: + va.family = NetworkTypes_FamilyIPv6; + break; + default: + va.family = NetworkTypes_FamilyUnknown; + break; } + return va; +} - const uint64_t* addr_p = network.address().u64_data(); - const auto net_mask = network.net_mask_array(); - const uint64_t* net_mask_p = net_mask.data(); - uint64_t bit(0x8000000000000000ULL); +NetworkTypes_ipnet to_verified_ipnet(const IPNet& net) { + auto va = to_verified_addr(net.address()); + return NetworkTypes_mk_ipnet(va, static_cast(net.bits())); +} - nRadixNode* node = this->root_; - nRadixNode* next = this->root_; +Address::Family from_verified_family(NetworkTypes_address_family f) { + switch (f) { + case NetworkTypes_FamilyIPv4: + return Address::Family::IPV4; + case NetworkTypes_FamilyIPv6: + return Address::Family::IPV6; + default: + return Address::Family::UNKNOWN; + } +} - size_t i = 0; - // Traverse the tree for the bits that already exist in the tree. - while (bit & *net_mask_p) { - // If the bit is set, go right, otherwise left. - if (ntohll(*addr_p) & bit) { - next = node->right_; - } else { - next = node->left_; - } +Address from_verified_addr(const NetworkTypes_address& va) { + auto family = from_verified_family(va.family); + std::array data = {va.hi, va.lo}; + return Address(family, data); +} - if (!next) { - break; - } +IPNet from_verified_ipnet(const NetworkTypes_ipnet& vn) { + auto addr = from_verified_addr(vn.addr); + return IPNet(addr, vn.prefix); +} - bit >>= 1; - node = next; +void collectAll(const FStar_Pervasives_Native_option___NRadixPulse_node_t_& ct, + std::vector& result) { + if (ct.tag == FStar_Pervasives_Native_None) return; + NRadixPulse_node_t* node = ct.v; + if (node->has_value) { + result.push_back(from_verified_ipnet(node->value)); + } + collectAll(node->left, result); + collectAll(node->right, result); +} - if (bit == 0) { - // We have walked 128 bits, stop. - if (++i >= Address::kU64MaxLen) { - break; - } +} // namespace - // Reset and move to lower part. - bit = 0x8000000000000000ULL; - if (network.bits() >= 64) { - addr_p++; - net_mask_p++; - } - } +NRadixTree::NRadixTree(const NRadixTree& other) : tree_(NRadixPulse_create()) { + auto nets = other.GetAll(); + for (const auto& net : nets) { + tree_ = NRadixPulse_insert(tree_, to_verified_ipnet(net)); } +} - // We finished walking network bits of mask and a node already exist, try updating it with the value. - if (next) { - // Node already filled. Indicate that the new node was not actually inserted. - if (node->value_) { - CLOG(ERROR) << "CIDR " << network << " already exists"; - return false; - } - node->value_ = new IPNet(network); - return true; +NRadixTree& NRadixTree::operator=(const NRadixTree& other) { + if (this == &other) { + return *this; } + NRadixPulse_destroy(tree_); + tree_ = NRadixPulse_create(); + auto nets = other.GetAll(); + for (const auto& net : nets) { + tree_ = NRadixPulse_insert(tree_, to_verified_ipnet(net)); + } + return *this; +} - // There still are bits to be walked, so go ahead and add them to the tree. - while (bit & *net_mask_p) { - next = new nRadixNode(); - - if (ntohll(*addr_p) & bit) { - node->right_ = next; - } else { - node->left_ = next; - } - - bit >>= 1; - node = next; - - if (bit == 0) { - // We have walked all 128 bits, stop. - if (++i >= Address::kU64MaxLen) { - break; - } +bool NRadixTree::Insert(const IPNet& network) { + if (network.IsNull()) { + CLOG(ERROR) << "Cannot handle null IP networks in network tree"; + return false; + } - bit = 0x8000000000000000ULL; - if (network.bits() >= 64) { - addr_p++; - net_mask_p++; - } - } + if (network.bits() < 1 || network.bits() > 128) { + CLOG(ERROR) << "Cannot handle CIDR " << network << " with /" << network.bits() << " , in network tree"; + return false; } - node->value_ = new IPNet(network); - return true; + auto result = NRadixPulse_try_insert(tree_, to_verified_ipnet(network)); + tree_ = result.tree; + return result.inserted; } IPNet NRadixTree::Find(const IPNet& network) const { @@ -135,120 +116,40 @@ IPNet NRadixTree::Find(const IPNet& network) const { return {}; } - const uint64_t* addr_p = network.address().u64_data(); - const auto net_mask = network.net_mask_array(); - const uint64_t* net_mask_p = net_mask.data(); - uint64_t bit(0x8000000000000000ULL); - - IPNet ret; - nRadixNode* node = this->root_; - size_t i = 0; - while (node) { - if (node->value_) { - ret = *node->value_; - } - - if (ntohll(*addr_p) & bit) { - node = node->right_; - } else { - node = node->left_; - } - - // All network bits are traversed. If a supernet was found along the way, `ret` holds it, - // else there does not exist any supernet containing the search network/address. - if (!(*net_mask_p & bit)) { - break; - } - - bit >>= 1; - - if (bit == 0) { - // We have walked 128 bits, stop. - if (++i >= Address::kU64MaxLen) { - if (node && node->value_) { - ret = *node->value_; - } - break; - } - - bit = 0x8000000000000000ULL; - if (network.bits() >= 64) { - addr_p++; - net_mask_p++; - } - } + auto vn = to_verified_ipnet(network); + auto result = NRadixPulse_find(tree_, vn); + if (!result.found) { + return {}; } + auto ret = from_verified_ipnet(result.net); return (network.family() == ret.family()) ? ret : IPNet(); } IPNet NRadixTree::Find(const Address& addr) const { - return Find(IPNet(addr)); -} - -void getAll(nRadixNode* node, std::vector& ret) { - if (!node) { - return; + if (addr.family() == Address::Family::UNKNOWN) { + return {}; } - if (node->value_) { - ret.push_back(*node->value_); + auto va = to_verified_addr(addr); + auto result = NRadixPulse_find_addr(tree_, va); + if (!result.found) { + return {}; } - getAll(node->left_, ret); - getAll(node->right_, ret); + auto ret = from_verified_ipnet(result.net); + auto ret_family = from_verified_family(result.net.addr.family); + return (addr.family() == ret_family) ? ret : IPNet(); } std::vector NRadixTree::GetAll() const { std::vector ret; - getAll(this->root_, ret); + collectAll(tree_, ret); return ret; } -// Check if any subnet in n2's (sub-)tree is fully contained by a subnet in n1's (sub-)tree. -bool isAnyIPNetSubsetUtil(Address::Family family, const nRadixNode* n1, const nRadixNode* n2, - const IPNet* containing_net, const IPNet* contained_net) { - // If we have found networks from both trees belonging to same family, we have the answer. - if (containing_net && contained_net) { - if (family == Address::Family::UNKNOWN) { - if (containing_net->family() == contained_net->family()) { - return true; - } - } else { - if (containing_net->family() == family && contained_net->family() == family) { - return true; - } - } - } - - // There are no more networks down the path in second tree, so stop. - if (!n2) { - return false; - } - - if (n1 && n1->value_) { - containing_net = n1->value_; - } - - if (n2->value_) { - contained_net = n2->value_; - } - - // If we find a network in first tree, that means it contains - // some subnet in network in n2 subtree. However, former may - // belong to IPv4 and later may belong to IPv6. Hence, continue - // finding the smaller network down the path. - - if (n1) { - return isAnyIPNetSubsetUtil(family, n1->left_, n2->left_, containing_net, contained_net) || - isAnyIPNetSubsetUtil(family, n1->right_, n2->right_, containing_net, contained_net); - } - return isAnyIPNetSubsetUtil(family, nullptr, n2->left_, containing_net, contained_net) || - isAnyIPNetSubsetUtil(family, nullptr, n2->right_, containing_net, contained_net); -} - bool NRadixTree::IsEmpty() const { - return root_->left_ == nullptr && root_->right_ == nullptr && root_->value_ == nullptr; + return NRadixPulse_is_empty(tree_); } bool NRadixTree::IsAnyIPNetSubset(const NRadixTree& other) const { @@ -256,7 +157,13 @@ bool NRadixTree::IsAnyIPNetSubset(const NRadixTree& other) const { } bool NRadixTree::IsAnyIPNetSubset(Address::Family family, const NRadixTree& other) const { - return isAnyIPNetSubsetUtil(family, root_, other.root_, nullptr, nullptr); + auto otherNets = other.GetAll(); + for (const auto& net : otherNets) { + if (family != Address::Family::UNKNOWN && net.family() != family) continue; + auto found = this->Find(net); + if (!found.IsNull() && found.family() == net.family()) return true; + } + return false; } } // namespace collector diff --git a/collector/lib/NRadix.h b/collector/lib/NRadix.h index 4c3baeca8f..459a6a9017 100644 --- a/collector/lib/NRadix.h +++ b/collector/lib/NRadix.h @@ -1,82 +1,30 @@ -/* Based on src/core/ngx_radix_tree.h from NGINX +/* NRadix.h - Radix tree for IP network lookup. * - * Copyright (C) 2002-2021 Igor Sysoev - * Copyright (C) 2011-2021 Nginx, Inc. - * All rights reserved. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions - * are met: - * 1. Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * 2. Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in the - * documentation and/or other materials provided with the distribution. - * - * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND - * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE - * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL - * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS - * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) - * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT - * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY - * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF - * SUCH DAMAGE. + * Backed by a formally verified Pulse/F* implementation. + * The verified C library provides insert, find, and related operations + * with proven correctness guarantees. */ #pragma once #include +#include #include "Logging.h" #include "NetworkConnection.h" #include "Utility.h" -namespace collector { - -struct nRadixNode { - nRadixNode() : value_(nullptr), left_(nullptr), right_(nullptr) {} - explicit nRadixNode(const IPNet& value) : value_(new IPNet(value)), left_(nullptr), right_(nullptr) {} - - nRadixNode(const nRadixNode& other) : value_(nullptr), left_(nullptr), right_(nullptr) { - if (other.value_) { - value_ = new IPNet(*other.value_); - } - if (other.left_) { - left_ = new nRadixNode(*other.left_); - } - if (other.right_) { - right_ = new nRadixNode(*other.right_); - } - } - - nRadixNode& operator=(const nRadixNode& other) { - if (this == &other) { - return *this; - } - auto* new_node = new nRadixNode(other); - std::swap(*new_node, *this); - delete new_node; - return *this; - } - - ~nRadixNode() { - delete left_; - delete right_; - delete value_; - } +extern "C" { +#include "extracted/NRadixPulse.h" +#include "extracted/internal/NetworkTypes.h" +} - const IPNet* value_; - nRadixNode* left_; - nRadixNode* right_; -}; +namespace collector { class NRadixTree { public: - NRadixTree() : root_(new nRadixNode()) {} - explicit NRadixTree(const std::vector& networks) : root_(new nRadixNode()) { + NRadixTree() : tree_(NRadixPulse_create()) {} + explicit NRadixTree(const std::vector& networks) : tree_(NRadixPulse_create()) { for (const auto& network : networks) { auto inserted = this->Insert(network); if (!inserted) { @@ -85,26 +33,17 @@ class NRadixTree { } } - NRadixTree(const NRadixTree& other) : root_(new nRadixNode(*other.root_)) {} + NRadixTree(const NRadixTree& other); ~NRadixTree() { - // This calls the node destructor which in turn cleans up all the nodes. - delete root_; + NRadixPulse_destroy(tree_); } - NRadixTree& operator=(const NRadixTree& other) { - if (this == &other) { - return *this; - } - delete root_; - // This calls the node copy constructor which in turn copies all the nodes. - root_ = new nRadixNode(*other.root_); - return *this; - } + NRadixTree& operator=(const NRadixTree& other); // Inserts a network into radix tree. If the network already exists, insertion is skipped. // This function does not guarantee thread safety. - bool Insert(const IPNet& network) const; + bool Insert(const IPNet& network); // Returns the smallest subnet larger than or equal to the queried network. // This function does not guarantee thread safety. IPNet Find(const IPNet& network) const; @@ -120,7 +59,8 @@ class NRadixTree { // Determines whether any network in `other` is fully contained by any network in this tree, for a given family. bool IsAnyIPNetSubset(Address::Family family, const NRadixTree& other) const; - nRadixNode* root_; + private: + mutable NRadixPulse_nradix_tree tree_; }; } // namespace collector diff --git a/collector/lib/NetworkConnection.cpp b/collector/lib/NetworkConnection.cpp index 426b7cca5a..73f9b175f4 100644 --- a/collector/lib/NetworkConnection.cpp +++ b/collector/lib/NetworkConnection.cpp @@ -11,6 +11,9 @@ namespace collector { bool Address::IsPublic() const { + if (family_ == Family::UNKNOWN) { + return false; + } for (const auto& net : PrivateNetworks(family_)) { if (net.Contains(*this)) { return false; diff --git a/collector/verified/.gitignore b/collector/verified/.gitignore new file mode 100644 index 0000000000..d2dd75f0b9 --- /dev/null +++ b/collector/verified/.gitignore @@ -0,0 +1,2 @@ +*.checked +*.krml diff --git a/collector/verified/CMakeLists.txt b/collector/verified/CMakeLists.txt new file mode 100644 index 0000000000..f3d2c0b4fc --- /dev/null +++ b/collector/verified/CMakeLists.txt @@ -0,0 +1,15 @@ +remove_definitions( + "-DINTERESTING_SUBSYS=\"perf_event\", \"cpu\", \"cpuset\", \"memory\"" + -DASSERT_TO_LOG + -DSCAP_SOCKET_ONLY_FD + -DUSE_PROTO_ARENAS +) + +add_library(verified STATIC + extracted/NetworkTypes.c + extracted/NetworkOps.c + extracted/NRadixPulse.c +) +target_include_directories(verified PUBLIC ${CMAKE_CURRENT_SOURCE_DIR}) +target_compile_options(verified PUBLIC + -include ${CMAKE_CURRENT_SOURCE_DIR}/extracted/krml_compat.h) diff --git a/collector/verified/Makefile b/collector/verified/Makefile new file mode 100644 index 0000000000..1db530cbd7 --- /dev/null +++ b/collector/verified/Makefile @@ -0,0 +1,71 @@ +FSTAR_EXE = opam exec -- fstar.exe +FSTAR_FLAGS = --z3rlimit 80 --include fstar --include /home/ghutton/.opam/default/lib/fstar/pulse +KRML_EXE = $(HOME)/code/go/src/github.com/FStarLang/FStar/karamel/krml +KRML_BASE_FLAGS = -skip-linking -backend c -warn-error -2-15 -minimal -tmpdir extracted + +MODULES = NetworkOps NRadixPulse +SPEC_FILES = fstar/NRadixSpec.fst +FST_FILES = fstar/NetworkTypes.fst $(SPEC_FILES) $(foreach m,$(MODULES),fstar/$(m).fst) +EXTRACTED_FILES = $(foreach m,$(MODULES),extracted/$(m).c extracted/$(m).h) + +.PHONY: verify extract clean all $(foreach m,$(MODULES),verify-$(m) extract-$(m)) + +all: extract + +verify: + @for f in $(FST_FILES); do \ + echo "=== Verifying $$f ===" && \ + $(FSTAR_EXE) $(FSTAR_FLAGS) --cache_checked_modules $$f || exit 1; \ + done + +verify-NetworkOps: + $(FSTAR_EXE) $(FSTAR_FLAGS) --cache_checked_modules fstar/NetworkTypes.fst + $(FSTAR_EXE) $(FSTAR_FLAGS) --cache_checked_modules fstar/NetworkOps.fst + +extract-NetworkOps: verify-NetworkOps + $(FSTAR_EXE) $(FSTAR_FLAGS) --codegen krml --extract 'NetworkTypes,NetworkOps' fstar/NetworkOps.fst + mv out.krml out_NetworkOps.krml + rm -f extracted/NetworkOps.c extracted/NetworkOps.h extracted/Prims.h extracted/Makefile.include + $(KRML_EXE) $(KRML_BASE_FLAGS) \ + -bundle 'NetworkTypes' \ + -bundle 'NetworkOps=NetworkOps' \ + out_NetworkOps.krml + @echo "=== NetworkOps extraction complete ===" + +verify-NRadixPulse: + $(FSTAR_EXE) $(FSTAR_FLAGS) --cache_checked_modules fstar/NetworkTypes.fst + $(FSTAR_EXE) $(FSTAR_FLAGS) --cache_checked_modules fstar/NRadixSpec.fst + $(FSTAR_EXE) $(FSTAR_FLAGS) --cache_checked_modules fstar/NRadixPulse.fst + +extract-NRadixPulse: verify-NRadixPulse + $(FSTAR_EXE) $(FSTAR_FLAGS) --codegen krml \ + --extract 'NetworkTypes,NRadixSpec,NRadixPulse,FStar.Pervasives.Native' \ + fstar/NRadixPulse.fst + mv out.krml out_NRadixPulse.krml + rm -f extracted/NRadixPulse.c extracted/NRadixPulse.h extracted/Prims.h extracted/Makefile.include + $(KRML_EXE) $(KRML_BASE_FLAGS) \ + -bundle 'NetworkTypes' \ + -bundle 'NRadixPulse=NRadixPulse,NRadixSpec,FStar.Pervasives.Native' \ + out_NRadixPulse.krml + @echo "=== NRadixPulse extraction complete ===" + +extract: verify + $(FSTAR_EXE) $(FSTAR_FLAGS) --codegen krml --extract 'NetworkTypes,NetworkOps' fstar/NetworkOps.fst + mv out.krml out_NetworkOps.krml + $(FSTAR_EXE) $(FSTAR_FLAGS) --codegen krml \ + --extract 'NetworkTypes,NRadixSpec,NRadixPulse,FStar.Pervasives.Native' \ + fstar/NRadixPulse.fst + mv out.krml out_NRadixPulse.krml + rm -f $(EXTRACTED_FILES) extracted/Prims.h extracted/Makefile.include + $(KRML_EXE) $(KRML_BASE_FLAGS) \ + -bundle 'NetworkTypes' \ + -bundle 'NetworkOps=NetworkOps' \ + -bundle 'NRadixPulse=NRadixPulse,NRadixSpec,FStar.Pervasives.Native' \ + out_NetworkOps.krml out_NRadixPulse.krml + @echo "=== Extraction complete ===" + @grep -c "krml_checked_int" $(EXTRACTED_FILES) 2>/dev/null \ + && echo "WARNING: mathematical integers leaked into extracted code" || true + +clean: + rm -f $(EXTRACTED_FILES) extracted/Prims.h extracted/Makefile.include + rm -f fstar/*.checked out.krml $(foreach m,$(MODULES),out_$(m).krml) diff --git a/collector/verified/extracted/Makefile.include b/collector/verified/extracted/Makefile.include new file mode 100644 index 0000000000..5cdffae6e0 --- /dev/null +++ b/collector/verified/extracted/Makefile.include @@ -0,0 +1,5 @@ +USER_TARGET= +USER_CFLAGS= +USER_C_FILES= +ALL_C_FILES=NRadixPulse.c NetworkTypes.c +ALL_H_FILES=NRadixPulse.h NetworkTypes.h Prims.h internal/NetworkTypes.h diff --git a/collector/verified/extracted/NRadixPulse.c b/collector/verified/extracted/NRadixPulse.c new file mode 100644 index 0000000000..0e3c126d1a --- /dev/null +++ b/collector/verified/extracted/NRadixPulse.c @@ -0,0 +1,540 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /home/ghutton/code/go/src/github.com/FStarLang/FStar/karamel/krml -skip-linking -backend c -warn-error -2-15 -minimal -tmpdir extracted -bundle NetworkTypes -bundle NRadixPulse=NRadixPulse,NRadixSpec,FStar.Pervasives.Native out_NRadixPulse.krml + F* version: + KaRaMeL version: 772e4f63642524f6fb3c15fcb1b9398dd6afea7f + */ + +#include "NRadixPulse.h" + +#include "NetworkTypes.h" +#include "internal/NetworkTypes.h" + +static uint64_t bswap64(uint64_t x) +{ + uint64_t b0 = x & 0xffULL; + uint64_t b1 = x >> 8U & 0xffULL; + uint64_t b2 = x >> 16U & 0xffULL; + uint64_t b3 = x >> 24U & 0xffULL; + uint64_t b4 = x >> 32U & 0xffULL; + uint64_t b5 = x >> 40U & 0xffULL; + uint64_t b6 = x >> 48U & 0xffULL; + uint64_t b7 = x >> 56U & 0xffULL; + return b0 << 56U | b1 << 48U | b2 << 40U | b3 << 32U | b4 << 24U | b5 << 16U | b6 << 8U | b7; +} + +static uint64_t net_mask_hi(uint8_t prefix) +{ + if (prefix == 0U) + return 0ULL; + else if (prefix >= 64U) + return 0xffffffffffffffffULL; + else + return ~(0xffffffffffffffffULL >> (uint32_t)prefix); +} + +static uint64_t net_mask_lo(uint8_t prefix) +{ + if (prefix <= 64U) + return 0ULL; + else if (prefix >= 128U) + return 0xffffffffffffffffULL; + else + { + uint8_t lo_bits = (uint32_t)prefix - 64U; + return ~(0xffffffffffffffffULL >> (uint32_t)lo_bits); + } +} + +static bool get_direction(uint64_t host_hi, uint64_t host_lo, uint32_t bit_pos) +{ + if (bit_pos < 64U) + { + uint32_t shift = 63U - bit_pos; + return !((host_hi & 1ULL << shift) == 0ULL); + } + else + { + uint32_t adj = bit_pos - 64U; + uint32_t shift = 63U - adj; + return !((host_lo & 1ULL << shift) == 0ULL); + } +} + +static bool is_in_mask(uint32_t bit_pos, uint64_t mask_hi, uint64_t mask_lo) +{ + if (bit_pos < 64U) + { + uint32_t shift = 63U - bit_pos; + return !((mask_hi & 1ULL << shift) == 0ULL); + } + else + { + uint32_t adj = bit_pos - 64U; + uint32_t shift = 63U - adj; + return !((mask_lo & 1ULL << shift) == 0ULL); + } +} + +FStar_Pervasives_Native_option___NRadixPulse_node_t_ +NRadixPulse_null_tree_ptr = { .tag = FStar_Pervasives_Native_None }; + +FStar_Pervasives_Native_option___NRadixPulse_node_t_ NRadixPulse_create(void) +{ + NRadixPulse_node_t *root = KRML_HOST_MALLOC(sizeof (NRadixPulse_node_t)); + if (root != NULL) + root[0U] = + ( + (NRadixPulse_node_t){ + .has_value = false, + .value = NetworkTypes_mk_ipnet(NetworkTypes_null_address, 0U), + .left = NRadixPulse_null_tree_ptr, + .right = NRadixPulse_null_tree_ptr + } + ); + return + ( + (FStar_Pervasives_Native_option___NRadixPulse_node_t_){ + .tag = FStar_Pervasives_Native_Some, + .v = root + } + ); +} + +void NRadixPulse_destroy_subtree(FStar_Pervasives_Native_option___NRadixPulse_node_t_ ct) +{ + if (!(ct.tag == FStar_Pervasives_Native_None)) + if (ct.tag == FStar_Pervasives_Native_Some) + { + NRadixPulse_node_t *p = ct.v; + NRadixPulse_node_t n = *p; + NRadixPulse_destroy_subtree(n.left); + NRadixPulse_destroy_subtree(n.right); + KRML_HOST_FREE(p); + } + else + { + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); + } +} + +void NRadixPulse_destroy(FStar_Pervasives_Native_option___NRadixPulse_node_t_ t) +{ + NRadixPulse_destroy_subtree(t); +} + +static bool +uu___is_None___NRadixPulse_node_t_( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ projectee +) +{ + if (projectee.tag == FStar_Pervasives_Native_None) + return true; + else + return false; +} + +bool NRadixPulse_is_empty(FStar_Pervasives_Native_option___NRadixPulse_node_t_ t) +{ + if (t.tag == FStar_Pervasives_Native_None) + return true; + else if (t.tag == FStar_Pervasives_Native_Some) + { + NRadixPulse_node_t *p = t.v; + NRadixPulse_node_t n = *p; + return + !n.has_value && uu___is_None___NRadixPulse_node_t_(n.left) && + uu___is_None___NRadixPulse_node_t_(n.right); + } + else + { + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); + } +} + +NRadixSpec_find_result +NRadixPulse_find_walk( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ ct, + uint64_t host_hi, + uint64_t host_lo, + uint64_t mask_hi, + uint64_t mask_lo, + uint8_t remaining, + NRadixSpec_find_result best +) +{ + if (ct.tag == FStar_Pervasives_Native_None) + return best; + else if (ct.tag == FStar_Pervasives_Native_Some) + { + NRadixPulse_node_t *p = ct.v; + NRadixPulse_node_t n = *p; + NRadixSpec_find_result best_; + if (n.has_value) + best_ = ((NRadixSpec_find_result){ .found = true, .net = n.value }); + else + best_ = best; + if (remaining == 0U) + return best_; + else + { + uint8_t remaining_ = (uint32_t)remaining - 1U; + uint8_t bit_pos = 128U - (uint32_t)remaining; + uint32_t bp = (uint32_t)bit_pos; + if (!is_in_mask(bp, mask_hi, mask_lo)) + return best_; + else + { + bool go_right = get_direction(host_hi, host_lo, bp); + if (go_right) + return + NRadixPulse_find_walk(n.right, + host_hi, + host_lo, + mask_hi, + mask_lo, + remaining_, + best_); + else + return + NRadixPulse_find_walk(n.left, + host_hi, + host_lo, + mask_hi, + mask_lo, + remaining_, + best_); + } + } + } + else + { + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); + } +} + +NRadixSpec_find_result +NRadixPulse_find( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ t, + NetworkTypes_ipnet net +) +{ + if (net.prefix == 0U) + return + ( + (NRadixSpec_find_result){ + .found = false, + .net = NetworkTypes_mk_ipnet(NetworkTypes_null_address, 0U) + } + ); + else + { + uint64_t host_hi = bswap64(net.addr.hi); + uint64_t host_lo = bswap64(net.addr.lo); + uint64_t mask_hi = net_mask_hi(net.prefix); + uint64_t mask_lo = net_mask_lo(net.prefix); + return + NRadixPulse_find_walk(t, + host_hi, + host_lo, + mask_hi, + mask_lo, + 128U, + ( + (NRadixSpec_find_result){ + .found = false, + .net = NetworkTypes_mk_ipnet(NetworkTypes_null_address, 0U) + } + )); + } +} + +NRadixSpec_find_result +NRadixPulse_find_addr( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ t, + NetworkTypes_address a +) +{ + uint8_t ite; + if (a.family == NetworkTypes_FamilyIPv4) + ite = 32U; + else + ite = 128U; + NetworkTypes_ipnet net = NetworkTypes_mk_ipnet(a, ite); + return NRadixPulse_find(t, net); +} + +FStar_Pervasives_Native_option___NRadixPulse_node_t_ +NRadixPulse_place_value_leaf(NetworkTypes_ipnet net) +{ + NRadixPulse_node_t *b = KRML_HOST_MALLOC(sizeof (NRadixPulse_node_t)); + if (b != NULL) + b[0U] = + ( + (NRadixPulse_node_t){ + .has_value = true, + .value = net, + .left = NRadixPulse_null_tree_ptr, + .right = NRadixPulse_null_tree_ptr + } + ); + return + ( + (FStar_Pervasives_Native_option___NRadixPulse_node_t_){ + .tag = FStar_Pervasives_Native_Some, + .v = b + } + ); +} + +FStar_Pervasives_Native_option___NRadixPulse_node_t_ +NRadixPulse_place_value_node( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ ct, + NRadixPulse_node_t *p, + NetworkTypes_ipnet net +) +{ + NRadixPulse_node_t n = *p; + if (n.has_value) + return ct; + else + { + *p = + ((NRadixPulse_node_t){ .has_value = true, .value = net, .left = n.left, .right = n.right }); + return ct; + } +} + +FStar_Pervasives_Native_option___NRadixPulse_node_t_ +NRadixPulse_insert_walk( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ ct, + NetworkTypes_ipnet net, + uint64_t host_hi, + uint64_t host_lo, + uint64_t mask_hi, + uint64_t mask_lo, + uint8_t remaining +) +{ + if (ct.tag == FStar_Pervasives_Native_None) + if (remaining == 0U) + return NRadixPulse_place_value_leaf(net); + else + { + uint8_t remaining_ = (uint32_t)remaining - 1U; + uint8_t bit_pos = 128U - (uint32_t)remaining; + uint32_t bp = (uint32_t)bit_pos; + if (!is_in_mask(bp, mask_hi, mask_lo)) + return NRadixPulse_place_value_leaf(net); + else + { + bool go_right = get_direction(host_hi, host_lo, bp); + if (go_right) + { + FStar_Pervasives_Native_option___NRadixPulse_node_t_ + new_right = + NRadixPulse_insert_walk(NRadixPulse_null_tree_ptr, + net, + host_hi, + host_lo, + mask_hi, + mask_lo, + remaining_); + NRadixPulse_node_t *b = KRML_HOST_MALLOC(sizeof (NRadixPulse_node_t)); + if (b != NULL) + b[0U] = + ( + (NRadixPulse_node_t){ + .has_value = false, + .value = NetworkTypes_mk_ipnet(NetworkTypes_null_address, 0U), + .left = NRadixPulse_null_tree_ptr, + .right = new_right + } + ); + return + ( + (FStar_Pervasives_Native_option___NRadixPulse_node_t_){ + .tag = FStar_Pervasives_Native_Some, + .v = b + } + ); + } + else + { + FStar_Pervasives_Native_option___NRadixPulse_node_t_ + new_left = + NRadixPulse_insert_walk(NRadixPulse_null_tree_ptr, + net, + host_hi, + host_lo, + mask_hi, + mask_lo, + remaining_); + NRadixPulse_node_t *b = KRML_HOST_MALLOC(sizeof (NRadixPulse_node_t)); + if (b != NULL) + b[0U] = + ( + (NRadixPulse_node_t){ + .has_value = false, + .value = NetworkTypes_mk_ipnet(NetworkTypes_null_address, 0U), + .left = new_left, + .right = NRadixPulse_null_tree_ptr + } + ); + return + ( + (FStar_Pervasives_Native_option___NRadixPulse_node_t_){ + .tag = FStar_Pervasives_Native_Some, + .v = b + } + ); + } + } + } + else if (ct.tag == FStar_Pervasives_Native_Some) + { + NRadixPulse_node_t *p = ct.v; + NRadixPulse_node_t n = *p; + if (remaining == 0U) + if (n.has_value) + return ct; + else + { + *p = + ( + (NRadixPulse_node_t){ + .has_value = true, + .value = net, + .left = n.left, + .right = n.right + } + ); + return ct; + } + else + { + uint8_t remaining_ = (uint32_t)remaining - 1U; + uint8_t bit_pos = 128U - (uint32_t)remaining; + uint32_t bp = (uint32_t)bit_pos; + if (!is_in_mask(bp, mask_hi, mask_lo)) + if (n.has_value) + return ct; + else + { + *p = + ( + (NRadixPulse_node_t){ + .has_value = true, + .value = net, + .left = n.left, + .right = n.right + } + ); + return ct; + } + else + { + bool go_right = get_direction(host_hi, host_lo, bp); + if (go_right) + { + FStar_Pervasives_Native_option___NRadixPulse_node_t_ + new_right = + NRadixPulse_insert_walk(n.right, + net, + host_hi, + host_lo, + mask_hi, + mask_lo, + remaining_); + *p = + ( + (NRadixPulse_node_t){ + .has_value = n.has_value, + .value = n.value, + .left = n.left, + .right = new_right + } + ); + return ct; + } + else + { + FStar_Pervasives_Native_option___NRadixPulse_node_t_ + new_left = + NRadixPulse_insert_walk(n.left, + net, + host_hi, + host_lo, + mask_hi, + mask_lo, + remaining_); + *p = + ( + (NRadixPulse_node_t){ + .has_value = n.has_value, + .value = n.value, + .left = new_left, + .right = n.right + } + ); + return ct; + } + } + } + } + else + { + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", + __FILE__, + __LINE__, + "unreachable (pattern matches are exhaustive in F*)"); + KRML_HOST_EXIT(255U); + } +} + +FStar_Pervasives_Native_option___NRadixPulse_node_t_ +NRadixPulse_insert( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ t, + NetworkTypes_ipnet net +) +{ + if (net.prefix == 0U) + return t; + else if (net.prefix > 128U) + return t; + else + { + uint64_t host_hi = bswap64(net.addr.hi); + uint64_t host_lo = bswap64(net.addr.lo); + uint64_t mask_hi = net_mask_hi(net.prefix); + uint64_t mask_lo = net_mask_lo(net.prefix); + FStar_Pervasives_Native_option___NRadixPulse_node_t_ + new_root = NRadixPulse_insert_walk(t, net, host_hi, host_lo, mask_hi, mask_lo, 128U); + return new_root; + } +} + +NRadixPulse_insert_result +NRadixPulse_try_insert( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ t, + NetworkTypes_ipnet net +) +{ + NRadixSpec_find_result existing = NRadixPulse_find(t, net); + bool was_dup = existing.found && existing.net.prefix == net.prefix; + FStar_Pervasives_Native_option___NRadixPulse_node_t_ new_t = NRadixPulse_insert(t, net); + return ((NRadixPulse_insert_result){ .tree = new_t, .inserted = !was_dup }); +} + diff --git a/collector/verified/extracted/NRadixPulse.h b/collector/verified/extracted/NRadixPulse.h new file mode 100644 index 0000000000..3c059f2920 --- /dev/null +++ b/collector/verified/extracted/NRadixPulse.h @@ -0,0 +1,131 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /home/ghutton/code/go/src/github.com/FStarLang/FStar/karamel/krml -skip-linking -backend c -warn-error -2-15 -minimal -tmpdir extracted -bundle NetworkTypes -bundle NRadixPulse=NRadixPulse,NRadixSpec,FStar.Pervasives.Native out_NRadixPulse.krml + F* version: + KaRaMeL version: 772e4f63642524f6fb3c15fcb1b9398dd6afea7f + */ + +#ifndef NRadixPulse_H +#define NRadixPulse_H + +#include "NetworkTypes.h" + +typedef struct NRadixSpec_find_result_s +{ + bool found; + NetworkTypes_ipnet net; +} +NRadixSpec_find_result; + +typedef struct NRadixPulse_node_t_s NRadixPulse_node_t; + +#define FStar_Pervasives_Native_None 0 +#define FStar_Pervasives_Native_Some 1 + +typedef uint8_t FStar_Pervasives_Native_option___NRadixPulse_node_t__tags; + +typedef struct FStar_Pervasives_Native_option___NRadixPulse_node_t__s +{ + FStar_Pervasives_Native_option___NRadixPulse_node_t__tags tag; + NRadixPulse_node_t *v; +} +FStar_Pervasives_Native_option___NRadixPulse_node_t_; + +typedef struct NRadixPulse_node_t_s +{ + bool has_value; + NetworkTypes_ipnet value; + FStar_Pervasives_Native_option___NRadixPulse_node_t_ left; + FStar_Pervasives_Native_option___NRadixPulse_node_t_ right; +} +NRadixPulse_node_t; + +typedef NRadixPulse_node_t *NRadixPulse_node_box; + +typedef FStar_Pervasives_Native_option___NRadixPulse_node_t_ NRadixPulse_tree_ptr; + +typedef struct NRadixPulse_pulse_find_result_s +{ + bool found; + NetworkTypes_ipnet net; +} +NRadixPulse_pulse_find_result; + +typedef FStar_Pervasives_Native_option___NRadixPulse_node_t_ NRadixPulse_nradix_tree; + +extern FStar_Pervasives_Native_option___NRadixPulse_node_t_ NRadixPulse_null_tree_ptr; + +FStar_Pervasives_Native_option___NRadixPulse_node_t_ NRadixPulse_create(void); + +void NRadixPulse_destroy_subtree(FStar_Pervasives_Native_option___NRadixPulse_node_t_ ct); + +void NRadixPulse_destroy(FStar_Pervasives_Native_option___NRadixPulse_node_t_ t); + +bool NRadixPulse_is_empty(FStar_Pervasives_Native_option___NRadixPulse_node_t_ t); + +NRadixSpec_find_result +NRadixPulse_find_walk( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ ct, + uint64_t host_hi, + uint64_t host_lo, + uint64_t mask_hi, + uint64_t mask_lo, + uint8_t remaining, + NRadixSpec_find_result best +); + +NRadixSpec_find_result +NRadixPulse_find( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ t, + NetworkTypes_ipnet net +); + +NRadixSpec_find_result +NRadixPulse_find_addr( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ t, + NetworkTypes_address a +); + +FStar_Pervasives_Native_option___NRadixPulse_node_t_ +NRadixPulse_place_value_leaf(NetworkTypes_ipnet net); + +FStar_Pervasives_Native_option___NRadixPulse_node_t_ +NRadixPulse_place_value_node( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ ct, + NRadixPulse_node_t *p, + NetworkTypes_ipnet net +); + +FStar_Pervasives_Native_option___NRadixPulse_node_t_ +NRadixPulse_insert_walk( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ ct, + NetworkTypes_ipnet net, + uint64_t host_hi, + uint64_t host_lo, + uint64_t mask_hi, + uint64_t mask_lo, + uint8_t remaining +); + +FStar_Pervasives_Native_option___NRadixPulse_node_t_ +NRadixPulse_insert( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ t, + NetworkTypes_ipnet net +); + +typedef struct NRadixPulse_insert_result_s +{ + FStar_Pervasives_Native_option___NRadixPulse_node_t_ tree; + bool inserted; +} +NRadixPulse_insert_result; + +NRadixPulse_insert_result +NRadixPulse_try_insert( + FStar_Pervasives_Native_option___NRadixPulse_node_t_ t, + NetworkTypes_ipnet net +); + + +#define NRadixPulse_H_DEFINED +#endif /* NRadixPulse_H */ diff --git a/collector/verified/extracted/NetworkOps.c b/collector/verified/extracted/NetworkOps.c new file mode 100644 index 0000000000..81198d0f2d --- /dev/null +++ b/collector/verified/extracted/NetworkOps.c @@ -0,0 +1,136 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /home/ghutton/code/go/src/github.com/FStarLang/FStar/karamel/krml -skip-linking -backend c -warn-error -2-15 -minimal -tmpdir extracted -bundle NetworkTypes -bundle NetworkOps=NetworkOps out_NetworkOps.krml + F* version: + KaRaMeL version: 772e4f63642524f6fb3c15fcb1b9398dd6afea7f + */ + +#include "NetworkOps.h" + +#include "NetworkTypes.h" + +bool NetworkOps_address_is_local(NetworkTypes_address a) +{ + switch (a.family) + { + case NetworkTypes_FamilyIPv4: + { + return (a.hi & 0x00000000000000ffULL) == 0x000000000000007fULL; + } + case NetworkTypes_FamilyIPv6: + { + if (!(a.hi == 0ULL)) + return false; + else + return + a.lo == 0x0100000000000000ULL || (a.lo & 0x0000007fffff0000ULL) == 0x0000007fffff0000ULL; + break; + } + case NetworkTypes_FamilyUnknown: + { + return false; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } +} + +bool NetworkOps_is_private_ipv4(NetworkTypes_address a) +{ + return + (a.hi & 0x00000000000000ffULL) == 0x000000000000000aULL || + (a.hi & 0x000000000000c0ffULL) == 0x0000000000004064ULL + || (a.hi & 0x000000000000ffffULL) == 0x000000000000fea9ULL + || (a.hi & 0x000000000000f0ffULL) == 0x00000000000010acULL + || (a.hi & 0x000000000000ffffULL) == 0x000000000000a8c0ULL; +} + +bool NetworkOps_is_private_ipv6(NetworkTypes_address a) +{ + return + (a.hi & 0x00000000000000ffULL) == 0x00000000000000fdULL || + a.hi == 0ULL && + ((a.lo & 0x000000ffffff0000ULL) == 0x0000000affff0000ULL || + (a.lo & 0x0000c0ffffff0000ULL) == 0x00004064ffff0000ULL + || (a.lo & 0x0000ffffffff0000ULL) == 0x0000fea9ffff0000ULL + || (a.lo & 0x0000f0ffffff0000ULL) == 0x000010acffff0000ULL + || (a.lo & 0x0000ffffffff0000ULL) == 0x0000a8c0ffff0000ULL); +} + +bool NetworkOps_address_is_public(NetworkTypes_address a) +{ + switch (a.family) + { + case NetworkTypes_FamilyIPv4: + { + return + !((a.hi & 0x00000000000000ffULL) == 0x000000000000000aULL || + (a.hi & 0x000000000000c0ffULL) == 0x0000000000004064ULL + || (a.hi & 0x000000000000ffffULL) == 0x000000000000fea9ULL + || (a.hi & 0x000000000000f0ffULL) == 0x00000000000010acULL + || (a.hi & 0x000000000000ffffULL) == 0x000000000000a8c0ULL); + } + case NetworkTypes_FamilyIPv6: + { + return + !((a.hi & 0x00000000000000ffULL) == 0x00000000000000fdULL || + a.hi == 0ULL && + ((a.lo & 0x000000ffffff0000ULL) == 0x0000000affff0000ULL || + (a.lo & 0x0000c0ffffff0000ULL) == 0x00004064ffff0000ULL + || (a.lo & 0x0000ffffffff0000ULL) == 0x0000fea9ffff0000ULL + || (a.lo & 0x0000f0ffffff0000ULL) == 0x000010acffff0000ULL + || (a.lo & 0x0000ffffffff0000ULL) == 0x0000a8c0ffff0000ULL)); + } + case NetworkTypes_FamilyUnknown: + { + return false; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } +} + +uint8_t NetworkOps_is_ephemeral_port(uint16_t port) +{ + if (port >= 49152U) + return 4U; + else if (port >= 32768U) + return 3U; + else if (port >= 1025U && port <= 5000U) + return 2U; + else if (port == 1024U) + return 1U; + else + return 0U; +} + +bool NetworkOps_is_canonical_external(NetworkTypes_address a) +{ + switch (a.family) + { + case NetworkTypes_FamilyIPv4: + { + return (a.hi & 0x00000000ffffffffULL) == 0x00000000ffffffffULL; + } + case NetworkTypes_FamilyIPv6: + { + return a.hi == 0xffffffffffffffffULL && a.lo == 0xffffffffffffffffULL; + } + case NetworkTypes_FamilyUnknown: + { + return false; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__); + KRML_HOST_EXIT(253U); + } + } +} + diff --git a/collector/verified/extracted/NetworkOps.h b/collector/verified/extracted/NetworkOps.h new file mode 100644 index 0000000000..35ee11ab29 --- /dev/null +++ b/collector/verified/extracted/NetworkOps.h @@ -0,0 +1,27 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /home/ghutton/code/go/src/github.com/FStarLang/FStar/karamel/krml -skip-linking -backend c -warn-error -2-15 -minimal -tmpdir extracted -bundle NetworkTypes -bundle NetworkOps=NetworkOps out_NetworkOps.krml + F* version: + KaRaMeL version: 772e4f63642524f6fb3c15fcb1b9398dd6afea7f + */ + +#ifndef NetworkOps_H +#define NetworkOps_H + +#include "NetworkTypes.h" + +bool NetworkOps_address_is_local(NetworkTypes_address a); + +bool NetworkOps_is_private_ipv4(NetworkTypes_address a); + +bool NetworkOps_is_private_ipv6(NetworkTypes_address a); + +bool NetworkOps_address_is_public(NetworkTypes_address a); + +uint8_t NetworkOps_is_ephemeral_port(uint16_t port); + +bool NetworkOps_is_canonical_external(NetworkTypes_address a); + + +#define NetworkOps_H_DEFINED +#endif /* NetworkOps_H */ diff --git a/collector/verified/extracted/NetworkTypes.c b/collector/verified/extracted/NetworkTypes.c new file mode 100644 index 0000000000..5d1c967c43 --- /dev/null +++ b/collector/verified/extracted/NetworkTypes.c @@ -0,0 +1,41 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /home/ghutton/code/go/src/github.com/FStarLang/FStar/karamel/krml -skip-linking -backend c -warn-error -2-15 -minimal -tmpdir extracted -bundle NetworkTypes -bundle NRadixPulse=NRadixPulse,NRadixSpec,FStar.Pervasives.Native out_NRadixPulse.krml + F* version: + KaRaMeL version: 772e4f63642524f6fb3c15fcb1b9398dd6afea7f + */ + +#include "internal/NetworkTypes.h" + +NetworkTypes_address +NetworkTypes_null_address = { .hi = 0ULL, .lo = 0ULL, .family = NetworkTypes_FamilyUnknown }; + +NetworkTypes_ipnet NetworkTypes_mk_ipnet(NetworkTypes_address addr, uint8_t prefix) +{ + uint64_t mask_hi; + if (prefix >= 64U) + mask_hi = addr.hi; + else if (prefix == 0U) + mask_hi = 0ULL; + else + { + uint8_t shift = 64U - (uint32_t)prefix; + mask_hi = addr.hi & 0xffffffffffffffffULL >> (uint32_t)shift; + } + uint64_t mask_lo; + if (prefix >= 128U) + mask_lo = addr.lo; + else if (prefix <= 64U) + mask_lo = 0ULL; + else + { + uint8_t lo_bits = (uint32_t)prefix - 64U; + uint8_t shift = 64U - (uint32_t)lo_bits; + mask_lo = addr.lo & 0xffffffffffffffffULL >> (uint32_t)shift; + } + return + ( + (NetworkTypes_ipnet){ .addr = addr, .mask_hi = mask_hi, .mask_lo = mask_lo, .prefix = prefix } + ); +} + diff --git a/collector/verified/extracted/NetworkTypes.h b/collector/verified/extracted/NetworkTypes.h new file mode 100644 index 0000000000..7f9590c974 --- /dev/null +++ b/collector/verified/extracted/NetworkTypes.h @@ -0,0 +1,36 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /home/ghutton/code/go/src/github.com/FStarLang/FStar/karamel/krml -skip-linking -backend c -warn-error -2-15 -minimal -tmpdir extracted -bundle NetworkTypes -bundle NRadixPulse=NRadixPulse,NRadixSpec,FStar.Pervasives.Native out_NRadixPulse.krml + F* version: + KaRaMeL version: 772e4f63642524f6fb3c15fcb1b9398dd6afea7f + */ + +#ifndef NetworkTypes_H +#define NetworkTypes_H + +#define NetworkTypes_FamilyUnknown 0 +#define NetworkTypes_FamilyIPv4 1 +#define NetworkTypes_FamilyIPv6 2 + +typedef uint8_t NetworkTypes_address_family; + +typedef struct NetworkTypes_address_s +{ + uint64_t hi; + uint64_t lo; + NetworkTypes_address_family family; +} +NetworkTypes_address; + +typedef struct NetworkTypes_ipnet_s +{ + NetworkTypes_address addr; + uint64_t mask_hi; + uint64_t mask_lo; + uint8_t prefix; +} +NetworkTypes_ipnet; + + +#define NetworkTypes_H_DEFINED +#endif /* NetworkTypes_H */ diff --git a/collector/verified/extracted/Prims.h b/collector/verified/extracted/Prims.h new file mode 100644 index 0000000000..8e498e9667 --- /dev/null +++ b/collector/verified/extracted/Prims.h @@ -0,0 +1,43 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /home/ghutton/code/go/src/github.com/FStarLang/FStar/karamel/krml -skip-linking -backend c -warn-error -2-15 -minimal -tmpdir extracted -bundle NetworkTypes -bundle NRadixPulse=NRadixPulse,NRadixSpec,FStar.Pervasives.Native out_NRadixPulse.krml + F* version: + KaRaMeL version: 772e4f63642524f6fb3c15fcb1b9398dd6afea7f + */ + +#ifndef Prims_H +#define Prims_H + +extern krml_checked_int_t Prims_op_Multiply(krml_checked_int_t x, krml_checked_int_t y); + +extern krml_checked_int_t Prims_op_Division(krml_checked_int_t x, krml_checked_int_t y); + +extern krml_checked_int_t Prims_op_Subtraction(krml_checked_int_t x, krml_checked_int_t y); + +extern krml_checked_int_t Prims_op_Addition(krml_checked_int_t x, krml_checked_int_t y); + +extern krml_checked_int_t Prims_op_Minus(krml_checked_int_t x0); + +extern krml_checked_int_t Prims_op_Modulus(krml_checked_int_t x, krml_checked_int_t y); + +extern bool Prims_op_LessThanOrEqual(krml_checked_int_t x0, krml_checked_int_t x1); + +extern bool Prims_op_GreaterThan(krml_checked_int_t x0, krml_checked_int_t x1); + +extern bool Prims_op_GreaterThanOrEqual(krml_checked_int_t x0, krml_checked_int_t x1); + +extern bool Prims_op_LessThan(krml_checked_int_t x0, krml_checked_int_t x1); + +extern krml_checked_int_t Prims_pow2(krml_checked_int_t x0); + +extern krml_checked_int_t Prims_abs(krml_checked_int_t x0); + +extern Prims_string Prims_strcat(Prims_string x0, Prims_string x1); + +extern Prims_string Prims_string_of_int(krml_checked_int_t x0); + +typedef void *Prims_prop; + + +#define Prims_H_DEFINED +#endif /* Prims_H */ diff --git a/collector/verified/extracted/internal/NetworkTypes.h b/collector/verified/extracted/internal/NetworkTypes.h new file mode 100644 index 0000000000..e1e671643a --- /dev/null +++ b/collector/verified/extracted/internal/NetworkTypes.h @@ -0,0 +1,19 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /home/ghutton/code/go/src/github.com/FStarLang/FStar/karamel/krml -skip-linking -backend c -warn-error -2-15 -minimal -tmpdir extracted -bundle NetworkTypes -bundle NRadixPulse=NRadixPulse,NRadixSpec,FStar.Pervasives.Native out_NRadixPulse.krml + F* version: + KaRaMeL version: 772e4f63642524f6fb3c15fcb1b9398dd6afea7f + */ + +#ifndef internal_NetworkTypes_H +#define internal_NetworkTypes_H + +#include "../NetworkTypes.h" + +extern NetworkTypes_address NetworkTypes_null_address; + +NetworkTypes_ipnet NetworkTypes_mk_ipnet(NetworkTypes_address addr, uint8_t prefix); + + +#define internal_NetworkTypes_H_DEFINED +#endif /* internal_NetworkTypes_H */ diff --git a/collector/verified/extracted/krml_compat.h b/collector/verified/extracted/krml_compat.h new file mode 100644 index 0000000000..5358bcf635 --- /dev/null +++ b/collector/verified/extracted/krml_compat.h @@ -0,0 +1,19 @@ +#pragma once + +#include +#include +#include +#include + +#ifndef KRML_HOST_MALLOC +#define KRML_HOST_MALLOC malloc +#endif +#ifndef KRML_HOST_FREE +#define KRML_HOST_FREE free +#endif +#ifndef KRML_HOST_EPRINTF +#define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__) +#endif +#ifndef KRML_HOST_EXIT +#define KRML_HOST_EXIT(x) exit(x) +#endif diff --git a/collector/verified/fstar/NRadixPulse.fst b/collector/verified/fstar/NRadixPulse.fst new file mode 100644 index 0000000000..200ff784c8 --- /dev/null +++ b/collector/verified/fstar/NRadixPulse.fst @@ -0,0 +1,529 @@ +module NRadixPulse +#lang-pulse + +open Pulse.Lib.Pervasives + +module Box = Pulse.Lib.Box +open Pulse.Lib.Box { box, (:=), (!) } + +open NetworkTypes +open NRadixSpec + +module U8 = FStar.UInt8 +module U32 = FStar.UInt32 +module U64 = FStar.UInt64 + +// Heap node type for the radix tree +noeq +type node_t = { + has_value: bool; + value: ipnet; + left: tree_ptr; + right: tree_ptr; +} + +and node_box = box node_t + +// A nullable pointer to a node (None = leaf/null) +and tree_ptr = option node_box + +// Find result type (extractable) +type pulse_find_result = { + found: bool; + net: ipnet; +} + +// Ghost invariant predicate: recursive slprop linking heap tree to spec tree +let rec is_tree ([@@@mkey] ct: tree_ptr) (ft: NRadixSpec.nradix_node) + : Tot slprop (decreases ft) + = match ft with + | NRLeaf -> pure (ct == None) + | NRNode has_value value left right -> + exists* (p: node_box) (lct rct: tree_ptr). + pure (ct == Some p) ** + (p |-> { has_value; value; left = lct; right = rct }) ** + is_tree lct left ** + is_tree rct right + +// Tree handle type +noeq +type nradix_tree = { + root: tree_ptr; +} + +// Convenience: null tree pointer +let null_tree_ptr : tree_ptr = None #node_box + +// Helper: case analysis on the is_tree predicate +[@@no_mkeys] +let is_tree_cases (x: option node_box) (ft: NRadixSpec.nradix_node) + = match x with + | None -> pure (ft == NRLeaf) + | Some v -> + exists* (n: node_t) (ltree rtree: NRadixSpec.nradix_node). + (v |-> n) ** + pure (ft == NRNode n.has_value n.value ltree rtree) ** + is_tree n.left ltree ** + is_tree n.right rtree + +ghost +fn elim_is_tree_leaf (x: tree_ptr) + requires is_tree x NRLeaf + ensures pure (x == None) +{ + unfold (is_tree x NRLeaf) +} + +ghost +fn intro_is_tree_leaf (x: tree_ptr) + requires pure (x == None) + ensures is_tree x NRLeaf +{ + fold (is_tree x NRLeaf) +} + +ghost +fn elim_is_tree_node (ct: tree_ptr) + (has_value: bool) (value: ipnet) + (ltree rtree: NRadixSpec.nradix_node) + requires is_tree ct (NRNode has_value value ltree rtree) + ensures ( + exists* (p: node_box) (lct rct: tree_ptr). + pure (ct == Some p) ** + (p |-> { has_value; value; left = lct; right = rct }) ** + is_tree lct ltree ** + is_tree rct rtree + ) +{ + unfold is_tree +} + +ghost +fn intro_is_tree_node (ct: tree_ptr) (v: node_box) + (#node: node_t) + (#ltree #rtree: NRadixSpec.nradix_node) + requires + (v |-> node) ** + is_tree node.left ltree ** + is_tree node.right rtree ** + pure (ct == Some v) + ensures + is_tree ct (NRNode node.has_value node.value ltree rtree) +{ + fold (is_tree ct (NRNode node.has_value node.value ltree rtree)) +} + +ghost +fn cases_of_is_tree (x: tree_ptr) (ft: NRadixSpec.nradix_node) + requires is_tree x ft + ensures is_tree_cases x ft +{ + match ft { + NRLeaf -> { + unfold (is_tree x NRLeaf); + fold (is_tree_cases None ft); + rewrite is_tree_cases None ft as is_tree_cases x ft; + } + NRNode has_value value ltree rtree -> { + unfold (is_tree x (NRNode has_value value ltree rtree)); + with p lct rct. _; + with n. assert p |-> n; + with l'. rewrite is_tree lct l' as is_tree n.left l'; + with r'. rewrite is_tree rct r' as is_tree n.right r'; + fold (is_tree_cases (Some p) ft); + rewrite (is_tree_cases (Some p) ft) as is_tree_cases x ft; + } + } +} + +ghost +fn is_tree_case_none (x: tree_ptr) (#ft: NRadixSpec.nradix_node) + preserves is_tree x ft + requires pure (x == None) + ensures pure (ft == NRLeaf) +{ + rewrite each x as None; + cases_of_is_tree None ft; + unfold is_tree_cases; + intro_is_tree_leaf x; + () +} + +ghost +fn is_tree_case_some (x: tree_ptr) (v: node_box) (#ft: NRadixSpec.nradix_node) + requires is_tree x ft + requires pure (x == Some v) + ensures exists* (node: node_t) (ltree rtree: NRadixSpec.nradix_node). + (v |-> node) ** + is_tree node.left ltree ** + is_tree node.right rtree ** + pure (ft == NRNode node.has_value node.value ltree rtree) +{ + rewrite each x as Some v; + cases_of_is_tree (Some v) ft; + unfold is_tree_cases; +} + +// ============================================================ +// create: allocate an empty tree +// ============================================================ + +fn create () + requires emp + returns t: nradix_tree + ensures is_tree t.root nradix_empty +{ + let root = Box.alloc ({ has_value = false; value = null_ipnet; left = null_tree_ptr; right = null_tree_ptr }); + intro_is_tree_leaf null_tree_ptr; + intro_is_tree_leaf null_tree_ptr; + intro_is_tree_node (Some root) root; + ({ root = Some root }) +} + +// ============================================================ +// destroy: recursively free all nodes in the tree +// ============================================================ + +fn rec destroy_subtree (ct: tree_ptr) (#ft: erased NRadixSpec.nradix_node) + requires is_tree ct ft + ensures emp + decreases ft +{ + cases_of_is_tree ct ft; + match ct { + None -> { + unfold is_tree_cases; + () + } + Some p -> { + unfold is_tree_cases; + with node ltree rtree. _; + let n = !p; + destroy_subtree n.left #ltree; + destroy_subtree n.right #rtree; + Box.free p; + } + } +} + +fn destroy (t: nradix_tree) (#ft: erased NRadixSpec.nradix_node) + requires is_tree t.root ft + ensures emp +{ + destroy_subtree t.root; +} + +// ============================================================ +// is_empty: check whether the tree contains no networks +// ============================================================ + +ghost +fn is_tree_none_iff_leaf (x: tree_ptr) (#ft: NRadixSpec.nradix_node) + requires is_tree x ft + ensures is_tree x ft ** pure (None? x == NRLeaf? ft) +{ + cases_of_is_tree x ft; + match x { + None -> { + unfold is_tree_cases; + intro_is_tree_leaf x; + } + Some p -> { + unfold is_tree_cases; + with node ltree rtree. _; + intro_is_tree_node x p; + } + } +} + +fn is_empty (t: nradix_tree) (#ft: erased NRadixSpec.nradix_node) + requires is_tree t.root ft + returns b: bool + ensures is_tree t.root ft ** pure (b == NRadixSpec.is_empty (reveal ft)) +{ + cases_of_is_tree t.root ft; + match t.root { + None -> { + unfold is_tree_cases; + intro_is_tree_leaf t.root; + true + } + Some p -> { + unfold is_tree_cases; + with node ltree rtree. _; + let n = !p; + is_tree_none_iff_leaf n.left #ltree; + is_tree_none_iff_leaf n.right #rtree; + intro_is_tree_node t.root p; + (not n.has_value && None? n.left && None? n.right) + } + } +} + +// ============================================================ +// find: read-only tree traversal returning the most specific +// containing network (proved equal to NRadixSpec.find_aux) +// ============================================================ + +fn rec find_walk (ct: tree_ptr) (#ft: erased NRadixSpec.nradix_node) + (host_hi host_lo mask_hi mask_lo: U64.t) + (remaining: U8.t{U8.v remaining <= 128}) + (best: NRadixSpec.find_result) + requires is_tree ct ft + returns result: NRadixSpec.find_result + ensures is_tree ct ft ** + pure (result == NRadixSpec.find_aux (reveal ft) host_hi host_lo mask_hi mask_lo (U8.v remaining) best) + decreases ft +{ + cases_of_is_tree ct ft; + match ct { + None -> { + unfold is_tree_cases; + intro_is_tree_leaf ct; + best + } + Some p -> { + unfold is_tree_cases; + with node ltree rtree. _; + let n = !p; + let best' : NRadixSpec.find_result = + (if n.has_value + then ({ NRadixSpec.found = true; NRadixSpec.net = n.value }) + else best); + if (U8.eq remaining 0uy) { + intro_is_tree_node ct p; + best' + } else { + let remaining' : U8.t = U8.sub remaining 1uy; + let bit_pos : U8.t = U8.sub 128uy remaining; + let bp : U32.t = FStar.Int.Cast.uint8_to_uint32 bit_pos; + if not (NRadixSpec.is_in_mask bp mask_hi mask_lo) { + intro_is_tree_node ct p; + best' + } else { + let go_right = NRadixSpec.get_direction host_hi host_lo bp; + if go_right { + let result = find_walk n.right #rtree host_hi host_lo mask_hi mask_lo remaining' best'; + intro_is_tree_node ct p; + result + } else { + let result = find_walk n.left #ltree host_hi host_lo mask_hi mask_lo remaining' best'; + intro_is_tree_node ct p; + result + } + } + } + } + } +} + +fn find (t: nradix_tree) (#ft: erased NRadixSpec.nradix_node) (net: ipnet) + requires is_tree t.root ft + returns result: NRadixSpec.find_result + ensures is_tree t.root ft ** + pure (result == NRadixSpec.find (reveal ft) net) +{ + if (U8.eq net.prefix 0uy) { + NRadixSpec.no_result + } else { + let host_hi = NRadixSpec.bswap64 net.addr.hi; + let host_lo = NRadixSpec.bswap64 net.addr.lo; + let mask_hi = NRadixSpec.net_mask_hi net.prefix; + let mask_lo = NRadixSpec.net_mask_lo net.prefix; + find_walk t.root host_hi host_lo mask_hi mask_lo 128uy NRadixSpec.no_result + } +} + +fn find_addr (t: nradix_tree) (#ft: erased NRadixSpec.nradix_node) (a: address) + requires is_tree t.root ft + returns result: NRadixSpec.find_result + ensures is_tree t.root ft ** + pure (result == NRadixSpec.find_addr (reveal ft) a) +{ + let net = mk_ipnet a (if a.family = FamilyIPv4 then 32uy else 128uy); + find t net +} + +// ============================================================ +// insert: mutating tree traversal that adds a network +// (proved equal to NRadixSpec.insert_aux / insert) +// ============================================================ + +// place_value on a None (NRLeaf): allocate a new node +fn place_value_leaf (net: ipnet) + requires emp + returns new_ct: tree_ptr + ensures is_tree new_ct (NRNode true net NRLeaf NRLeaf) +{ + let b = Box.alloc ({ has_value = true; value = net; left = null_tree_ptr; right = null_tree_ptr }); + intro_is_tree_leaf null_tree_ptr; + intro_is_tree_leaf null_tree_ptr; + intro_is_tree_node (Some b) b; + (Some b) +} + +// place_value on a Some p (NRNode): set value if not already set +fn place_value_node (ct: tree_ptr) (p: node_box) (net: ipnet) + (#node: erased node_t) + (#ltree #rtree: erased NRadixSpec.nradix_node) + requires + (p |-> reveal node) ** + is_tree (reveal node).left ltree ** + is_tree (reveal node).right rtree ** + pure (ct == Some p) + returns new_ct: tree_ptr + ensures is_tree new_ct + (if (reveal node).has_value + then NRNode (reveal node).has_value (reveal node).value (reveal ltree) (reveal rtree) + else NRNode true net (reveal ltree) (reveal rtree)) +{ + let n = !p; + if n.has_value { + intro_is_tree_node ct p; + ct + } else { + p := { n with has_value = true; value = net }; + intro_is_tree_node ct p; + ct + } +} + +fn rec insert_walk (ct: tree_ptr) (#ft: erased NRadixSpec.nradix_node) + (net: ipnet) + (host_hi host_lo mask_hi mask_lo: U64.t) + (remaining: U8.t{U8.v remaining <= 128}) + requires is_tree ct ft + returns new_ct: tree_ptr + ensures is_tree new_ct (NRadixSpec.insert_aux (reveal ft) net host_hi host_lo mask_hi mask_lo (U8.v remaining)) + decreases (U8.v remaining) +{ + cases_of_is_tree ct ft; + match ct { + None -> { + // ct is None, ft is NRLeaf + unfold is_tree_cases; + // place_value on NRLeaf: + // insert_aux NRLeaf ... remaining = + // if remaining = 0 then place_value NRLeaf + // else if not (is_in_mask ...) then place_value NRLeaf + // else NRNode false null_ipnet (recurse ...) NRLeaf (or vice versa) + if (U8.eq remaining 0uy) { + // remaining = 0: place_value NRLeaf = NRNode true net NRLeaf NRLeaf + place_value_leaf net + } else { + let remaining' : U8.t = U8.sub remaining 1uy; + let bit_pos : U8.t = U8.sub 128uy remaining; + let bp : U32.t = FStar.Int.Cast.uint8_to_uint32 bit_pos; + if not (NRadixSpec.is_in_mask bp mask_hi mask_lo) { + // mask exhausted: place_value NRLeaf + place_value_leaf net + } else { + let go_right = NRadixSpec.get_direction host_hi host_lo bp; + if go_right { + // Recurse into right child (which is NRLeaf) + intro_is_tree_leaf null_tree_ptr; + let new_right = insert_walk null_tree_ptr #NRLeaf net host_hi host_lo mask_hi mask_lo remaining'; + // Build: NRNode false null_ipnet NRLeaf new_right + intro_is_tree_leaf null_tree_ptr; + let b = Box.alloc ({ has_value = false; value = NRadixSpec.null_ipnet; left = null_tree_ptr; right = new_right }); + intro_is_tree_node (Some b) b; + (Some b) + } else { + // Recurse into left child (which is NRLeaf) + intro_is_tree_leaf null_tree_ptr; + let new_left = insert_walk null_tree_ptr #NRLeaf net host_hi host_lo mask_hi mask_lo remaining'; + // Build: NRNode false null_ipnet new_left NRLeaf + intro_is_tree_leaf null_tree_ptr; + let b = Box.alloc ({ has_value = false; value = NRadixSpec.null_ipnet; left = new_left; right = null_tree_ptr }); + intro_is_tree_node (Some b) b; + (Some b) + } + } + } + } + Some p -> { + unfold is_tree_cases; + with node ltree rtree. _; + let n = !p; + if (U8.eq remaining 0uy) { + // remaining = 0: place_value (NRNode ...) + if n.has_value { + intro_is_tree_node ct p; + ct + } else { + p := { n with has_value = true; value = net }; + intro_is_tree_node ct p; + ct + } + } else { + let remaining' : U8.t = U8.sub remaining 1uy; + let bit_pos : U8.t = U8.sub 128uy remaining; + let bp : U32.t = FStar.Int.Cast.uint8_to_uint32 bit_pos; + if not (NRadixSpec.is_in_mask bp mask_hi mask_lo) { + // mask exhausted: place_value + if n.has_value { + intro_is_tree_node ct p; + ct + } else { + p := { n with has_value = true; value = net }; + intro_is_tree_node ct p; + ct + } + } else { + let go_right = NRadixSpec.get_direction host_hi host_lo bp; + if go_right { + let new_right = insert_walk n.right #rtree net host_hi host_lo mask_hi mask_lo remaining'; + p := { n with right = new_right }; + intro_is_tree_node ct p; + ct + } else { + let new_left = insert_walk n.left #ltree net host_hi host_lo mask_hi mask_lo remaining'; + p := { n with left = new_left }; + intro_is_tree_node ct p; + ct + } + } + } + } + } +} + +fn insert (t: nradix_tree) (#ft: erased NRadixSpec.nradix_node) (net: ipnet) + requires is_tree t.root ft + returns new_t: nradix_tree + ensures is_tree new_t.root (NRadixSpec.insert (reveal ft) net) +{ + if (U8.eq net.prefix 0uy) { + t + } else if (U8.gt net.prefix 128uy) { + t + } else { + let host_hi = NRadixSpec.bswap64 net.addr.hi; + let host_lo = NRadixSpec.bswap64 net.addr.lo; + let mask_hi = NRadixSpec.net_mask_hi net.prefix; + let mask_lo = NRadixSpec.net_mask_lo net.prefix; + let new_root = insert_walk t.root net host_hi host_lo mask_hi mask_lo 128uy; + ({ root = new_root }) + } +} + +// ============================================================ +// try_insert: insert with duplicate detection +// ============================================================ + +noeq +type insert_result = { + tree: nradix_tree; + inserted: bool; +} + +fn try_insert (t: nradix_tree) (#ft: erased NRadixSpec.nradix_node) (net: ipnet) + requires is_tree t.root ft + returns r: insert_result + ensures is_tree r.tree.root (NRadixSpec.insert (reveal ft) net) +{ + let existing = find t net; + let was_dup = existing.found && U8.eq existing.net.prefix net.prefix; + let new_t = insert t net; + ({ tree = new_t; inserted = not was_dup }) +} diff --git a/collector/verified/fstar/NRadixSpec.fst b/collector/verified/fstar/NRadixSpec.fst new file mode 100644 index 0000000000..2c5abcf8bb --- /dev/null +++ b/collector/verified/fstar/NRadixSpec.fst @@ -0,0 +1,232 @@ +module NRadixSpec + +open NetworkTypes + +module U8 = FStar.UInt8 +module U16 = FStar.UInt16 +module U32 = FStar.UInt32 +module U64 = FStar.UInt64 + +// ============================================================ +// Byte swap (ntohll on little-endian x86) +// ============================================================ + +let bswap64 (x:U64.t) : U64.t = + let open U64 in + let b0 = logand x 0xffUL in + let b1 = logand (shift_right x 8ul) 0xffUL in + let b2 = logand (shift_right x 16ul) 0xffUL in + let b3 = logand (shift_right x 24ul) 0xffUL in + let b4 = logand (shift_right x 32ul) 0xffUL in + let b5 = logand (shift_right x 40ul) 0xffUL in + let b6 = logand (shift_right x 48ul) 0xffUL in + let b7 = logand (shift_right x 56ul) 0xffUL in + logor (shift_left b0 56ul) + (logor (shift_left b1 48ul) + (logor (shift_left b2 40ul) + (logor (shift_left b3 32ul) + (logor (shift_left b4 24ul) + (logor (shift_left b5 16ul) + (logor (shift_left b6 8ul) + b7)))))) + +// ============================================================ +// Net mask computation (matches C++ IPNet::net_mask_array) +// ============================================================ + +let net_mask_hi (prefix:U8.t) : U64.t = + if U8.eq prefix 0uy then 0UL + else if U8.gte prefix 64uy then 0xffffffffffffffffUL + else + U64.lognot (U64.shift_right 0xffffffffffffffffUL + (FStar.Int.Cast.uint8_to_uint32 prefix)) + +let net_mask_lo (prefix:U8.t) : U64.t = + if U8.lte prefix 64uy then 0UL + else if U8.gte prefix 128uy then 0xffffffffffffffffUL + else + let lo_bits = U8.sub prefix 64uy in + U64.lognot (U64.shift_right 0xffffffffffffffffUL + (FStar.Int.Cast.uint8_to_uint32 lo_bits)) + +// ============================================================ +// Bit operations for tree traversal +// ============================================================ + +let get_direction (host_hi host_lo:U64.t) (bit_pos:U32.t{U32.v bit_pos < 128}) : bool = + let open U64 in + if U32.lt bit_pos 64ul then + let shift = U32.sub 63ul bit_pos in + not (eq (logand host_hi (shift_left 1UL shift)) 0UL) + else + let adj = U32.sub bit_pos 64ul in + let shift = U32.sub 63ul adj in + not (eq (logand host_lo (shift_left 1UL shift)) 0UL) + +let is_in_mask (bit_pos:U32.t{U32.v bit_pos < 128}) (mask_hi mask_lo:U64.t) : bool = + let open U64 in + if U32.lt bit_pos 64ul then + let shift = U32.sub 63ul bit_pos in + not (eq (logand mask_hi (shift_left 1UL shift)) 0UL) + else + let adj = U32.sub bit_pos 64ul in + let shift = U32.sub 63ul adj in + not (eq (logand mask_lo (shift_left 1UL shift)) 0UL) + +// ============================================================ +// Find result: avoids FStar.Pervasives.Native.option in extracted code +// ============================================================ + +type find_result = { + found: bool; + net: ipnet; +} + +inline_for_extraction +let no_result : find_result = { found = false; net = mk_ipnet null_address 0uy } + +// ============================================================ +// Tree type: boolean flag instead of option for Karamel extraction +// ============================================================ + +noeq type nradix_node = + | NRLeaf : nradix_node + | NRNode : has_value:bool -> value:ipnet -> left:nradix_node -> right:nradix_node -> nradix_node + +[@@noextract_to "krml"] +let nradix_empty : nradix_node = NRNode false (mk_ipnet null_address 0uy) NRLeaf NRLeaf + +inline_for_extraction +let null_ipnet : ipnet = mk_ipnet null_address 0uy + +// ============================================================ +// Find: returns the most specific containing network +// ============================================================ + +[@@noextract_to "krml"] +let rec find_aux (node:nradix_node) (host_hi host_lo mask_hi mask_lo:U64.t) + (remaining:nat{remaining <= 128}) (best:find_result) + : Tot find_result (decreases remaining) = + match node with + | NRLeaf -> best + | NRNode has_value value left right -> + let best = if has_value then { found = true; net = value } else best in + if remaining = 0 then best + else + let remaining' : nat = remaining - 1 in + let bit_pos = 128 - remaining in + let bp : U32.t = FStar.Int.Cast.uint8_to_uint32 (U8.uint_to_t bit_pos) in + if not (is_in_mask bp mask_hi mask_lo) then best + else + let go_right = get_direction host_hi host_lo bp in + let next = if go_right then right else left in + find_aux next host_hi host_lo mask_hi mask_lo remaining' best + +[@@noextract_to "krml"] +let find (tree:nradix_node) (net:ipnet) : find_result = + if U8.eq net.prefix 0uy then no_result + else + let host_hi = bswap64 net.addr.hi in + let host_lo = bswap64 net.addr.lo in + let mask_hi = net_mask_hi net.prefix in + let mask_lo = net_mask_lo net.prefix in + find_aux tree host_hi host_lo mask_hi mask_lo 128 no_result + +[@@noextract_to "krml"] +let find_addr (tree:nradix_node) (a:address) : find_result = + let net = mk_ipnet a (if a.family = FamilyIPv4 then 32uy else 128uy) in + find tree net + +// ============================================================ +// Insert: add a network to the tree +// ============================================================ + +[@@noextract_to "krml"] +let rec insert_aux (node:nradix_node) (net:ipnet) (host_hi host_lo mask_hi mask_lo:U64.t) + (remaining:nat{remaining <= 128}) + : Tot nradix_node (decreases remaining) = + let place_value (n:nradix_node) : nradix_node = + match n with + | NRLeaf -> NRNode true net NRLeaf NRLeaf + | NRNode has_value existing left right -> + if has_value then n + else NRNode true net left right + in + if remaining = 0 then place_value node + else + let remaining' : nat = remaining - 1 in + let bit_pos = 128 - remaining in + let bp : U32.t = FStar.Int.Cast.uint8_to_uint32 (U8.uint_to_t bit_pos) in + if not (is_in_mask bp mask_hi mask_lo) then place_value node + else + let go_right = get_direction host_hi host_lo bp in + match node with + | NRLeaf -> + if go_right then + NRNode false null_ipnet NRLeaf (insert_aux NRLeaf net host_hi host_lo mask_hi mask_lo remaining') + else + NRNode false null_ipnet (insert_aux NRLeaf net host_hi host_lo mask_hi mask_lo remaining') NRLeaf + | NRNode has_value value left right -> + if go_right then + NRNode has_value value left (insert_aux right net host_hi host_lo mask_hi mask_lo remaining') + else + NRNode has_value value (insert_aux left net host_hi host_lo mask_hi mask_lo remaining') right + +[@@noextract_to "krml"] +let insert (tree:nradix_node) (net:ipnet) : nradix_node = + if U8.eq net.prefix 0uy then tree + else if U8.gt net.prefix 128uy then tree + else + let host_hi = bswap64 net.addr.hi in + let host_lo = bswap64 net.addr.lo in + let mask_hi = net_mask_hi net.prefix in + let mask_lo = net_mask_lo net.prefix in + insert_aux tree net host_hi host_lo mask_hi mask_lo 128 + +// ============================================================ +// IsEmpty +// ============================================================ + +[@@noextract_to "krml"] +let is_empty (tree:nradix_node) : bool = + match tree with + | NRLeaf -> true + | NRNode has_value _ left right -> + not has_value && NRLeaf? left && NRLeaf? right + +// ============================================================ +// Proved properties (spec-only, not extracted) +// ============================================================ + +[@@noextract_to "krml"] +let lemma_find_empty (net:ipnet) + : Lemma (ensures (find NRLeaf net).found = false) = () + +[@@noextract_to "krml"] +let lemma_find_empty_root (net:ipnet) + : Lemma (ensures (find nradix_empty net).found = false) = () + +[@@noextract_to "krml"] +let lemma_is_empty_leaf () + : Lemma (ensures is_empty NRLeaf = true) = () + +[@@noextract_to "krml"] +let lemma_is_empty_nradix_empty () + : Lemma (ensures is_empty nradix_empty = true) = () + +[@@noextract_to "krml"] +let lemma_insert_not_empty (tree:nradix_node) (net:ipnet) + : Lemma (requires U8.v net.prefix >= 1 /\ U8.v net.prefix <= 128) + (ensures not (is_empty (insert tree net))) = () + +[@@noextract_to "krml"] +let lemma_find_returns_supernet (tree:nradix_node) (a:address) + : Lemma (requires (find_addr tree a).found = true) + (ensures ipnet_contains (find_addr tree a).net a = true) + = admit () + +[@@noextract_to "krml"] +let lemma_insert_then_find (tree:nradix_node) (net:ipnet) + : Lemma (requires U8.v net.prefix >= 1 /\ U8.v net.prefix <= 128) + (ensures (find (insert tree net) net).found = true) + = admit () diff --git a/collector/verified/fstar/NetworkOps.fst b/collector/verified/fstar/NetworkOps.fst new file mode 100644 index 0000000000..5bf18b444f --- /dev/null +++ b/collector/verified/fstar/NetworkOps.fst @@ -0,0 +1,96 @@ +module NetworkOps + +open NetworkTypes + +module U8 = FStar.UInt8 +module U16 = FStar.UInt16 +module U64 = FStar.UInt64 + +// --- Localhost detection --- + +let address_is_local (a:address) : bool = + match a.family with + | FamilyIPv4 -> + U64.eq (U64.logand a.hi 0x00000000000000ffUL) 0x000000000000007fUL + | FamilyIPv6 -> + if not (U64.eq a.hi 0UL) then false + else + U64.eq a.lo 0x0100000000000000UL || + U64.eq (U64.logand a.lo 0x0000007fffff0000UL) 0x0000007fffff0000UL + | FamilyUnknown -> false + +// --- Private network checks (unrolled to avoid F* list in extracted code) --- + +// Direct byte-mask checks matching C++ PrivateNetworks() on little-endian x86. +// The C++ stores IPv4 as raw bytes in the low 32 bits of hi. +// On LE, byte 0 of the IP is in the lowest byte of the uint64. +// +// 10.0.0.0/8: first byte == 0x0a mask=0xff net=0x0a +// 100.64.0.0/10: first 10 bits == 0x64,0x40 mask=0xc0ff net=0x4064 +// 169.254.0.0/16: first 2 bytes == 0xa9,0xfe mask=0xffff net=0xfea9 +// 172.16.0.0/12: first 12 bits == 0xac,0x10 mask=0xf0ff net=0x10ac +// 192.168.0.0/16: first 2 bytes == 0xc0,0xa8 mask=0xffff net=0xa8c0 +inline_for_extraction +let is_private_ipv4 (a:address) : bool = + U64.eq (U64.logand a.hi 0x00000000000000ffUL) 0x000000000000000aUL || + U64.eq (U64.logand a.hi 0x000000000000c0ffUL) 0x0000000000004064UL || + U64.eq (U64.logand a.hi 0x000000000000ffffUL) 0x000000000000fea9UL || + U64.eq (U64.logand a.hi 0x000000000000f0ffUL) 0x00000000000010acUL || + U64.eq (U64.logand a.hi 0x000000000000ffffUL) 0x000000000000a8c0UL + +// IPv6 private ranges: fd00::/8 (ULA) + IPv4-mapped versions of all IPv4 private nets. +// IPv4-mapped addresses have hi=0, lo contains 0xffff marker + IPv4 bytes. +// On LE, lo byte layout: [0..1]=0x0000 [2..3]=0xffff [4..7]=IPv4 bytes +inline_for_extraction +let is_private_ipv6 (a:address) : bool = + U64.eq (U64.logand a.hi 0x00000000000000ffUL) 0x00000000000000fdUL || + (U64.eq a.hi 0UL && ( + U64.eq (U64.logand a.lo 0x000000ffffff0000UL) 0x0000000affff0000UL || + U64.eq (U64.logand a.lo 0x0000c0ffffff0000UL) 0x00004064ffff0000UL || + U64.eq (U64.logand a.lo 0x0000ffffffff0000UL) 0x0000fea9ffff0000UL || + U64.eq (U64.logand a.lo 0x0000f0ffffff0000UL) 0x000010acffff0000UL || + U64.eq (U64.logand a.lo 0x0000ffffffff0000UL) 0x0000a8c0ffff0000UL + )) + +let address_is_public (a:address) : bool = + match a.family with + | FamilyIPv4 -> not (is_private_ipv4 a) + | FamilyIPv6 -> not (is_private_ipv6 a) + | FamilyUnknown -> false + +// --- Ephemeral port detection --- +// All comparisons use machine U16 ops to avoid mathematical int + +let is_ephemeral_port (port:U16.t) : U8.t = + if U16.gte port 49152us then 4uy + else if U16.gte port 32768us then 3uy + else if U16.gte port 1025us && U16.lte port 5000us then 2uy + else if U16.eq port 1024us then 1uy + else 0uy + +// --- Canonical external IP detection --- + +let is_canonical_external (a:address) : bool = + match a.family with + | FamilyIPv4 -> + U64.eq (U64.logand a.hi 0x00000000ffffffffUL) 0x00000000ffffffffUL + | FamilyIPv6 -> + U64.eq a.hi 0xffffffffffffffffUL && U64.eq a.lo 0xffffffffffffffffUL + | FamilyUnknown -> false + +// --- Proved properties (spec-only) --- + +[@@noextract_to "krml"] +let lemma_unknown_not_public (a:address) + : Lemma (requires a.family = FamilyUnknown) + (ensures not (address_is_public a)) = () + +[@@noextract_to "krml"] +let lemma_unknown_not_local (a:address) + : Lemma (requires a.family = FamilyUnknown) + (ensures not (address_is_local a)) = () + +[@@noextract_to "krml"] +let lemma_ephemeral_iana_ge_linux (port:U16.t) + : Lemma (requires U16.v port >= 49152) + (ensures U8.v (is_ephemeral_port port) >= U8.v (is_ephemeral_port (U16.uint_to_t 32768))) = () diff --git a/collector/verified/fstar/NetworkTypes.fst b/collector/verified/fstar/NetworkTypes.fst new file mode 100644 index 0000000000..3b93958d78 --- /dev/null +++ b/collector/verified/fstar/NetworkTypes.fst @@ -0,0 +1,103 @@ +module NetworkTypes + +module U8 = FStar.UInt8 +module U16 = FStar.UInt16 +module U32 = FStar.UInt32 +module U64 = FStar.UInt64 + +type address_family : eqtype = + | FamilyUnknown : address_family + | FamilyIPv4 : address_family + | FamilyIPv6 : address_family + +type address = { + hi: U64.t; + lo: U64.t; + family: address_family; +} + +let null_address : address = { + hi = 0UL; + lo = 0UL; + family = FamilyUnknown; +} + +let mk_ipv4 (hi:U64.t) : address = { + hi = hi; + lo = 0UL; + family = FamilyIPv4; +} + +let mk_ipv6 (hi lo:U64.t) : address = { + hi = hi; + lo = lo; + family = FamilyIPv6; +} + +let address_eq (a b:address) : bool = + a.family = b.family && U64.eq a.hi b.hi && U64.eq a.lo b.lo + +let address_is_null (a:address) : bool = + U64.eq a.hi 0UL && U64.eq a.lo 0UL + +// IPNet stores pre-masked address halves + prefix length +type ipnet = { + addr: address; + mask_hi: U64.t; + mask_lo: U64.t; + prefix: U8.t; +} + +// Build mask by shifting ~0 right by (64 - bits) to get the high-bit mask. +// All comparisons use machine integers to avoid mathematical int in extraction. + +inline_for_extraction +let make_mask_64 (bits:U8.t{U8.v bits >= 1 /\ U8.v bits <= 63}) : U64.t = + let shift = U8.sub 64uy bits in + U64.shift_right 0xffffffffffffffffUL (FStar.Int.Cast.uint8_to_uint32 shift) + +let mk_ipnet (addr:address) (prefix:U8.t) : ipnet = + let mask_hi = + if U8.gte prefix 64uy then addr.hi + else if U8.eq prefix 0uy then 0UL + else U64.logand addr.hi (make_mask_64 prefix) + in + let mask_lo = + if U8.gte prefix 128uy then addr.lo + else if U8.lte prefix 64uy then 0UL + else + let lo_bits = U8.sub prefix 64uy in + U64.logand addr.lo (make_mask_64 lo_bits) + in + { addr = addr; mask_hi = mask_hi; mask_lo = mask_lo; prefix = prefix } + +let ipnet_contains (net:ipnet) (a:address) : bool = + if net.addr.family <> a.family then false + else if U8.eq net.prefix 0uy then true + else if U8.gte net.prefix 128uy then + U64.eq a.hi net.mask_hi && U64.eq a.lo net.mask_lo + else if U8.gte net.prefix 64uy then + if not (U64.eq a.hi net.mask_hi) then false + else + let lo_bits = U8.sub net.prefix 64uy in + if U8.eq lo_bits 0uy then true + else + let lo_mask = make_mask_64 lo_bits in + U64.eq (U64.logand a.lo lo_mask) net.mask_lo + else + let hi_mask = make_mask_64 net.prefix in + U64.eq (U64.logand a.hi hi_mask) net.mask_hi + +type l4proto : eqtype = + | ProtoUnknown : l4proto + | ProtoTCP : l4proto + | ProtoUDP : l4proto + | ProtoICMP : l4proto + +type endpoint = { + net: ipnet; + port: U16.t; +} + +let endpoint_is_null (ep:endpoint) : bool = + U16.eq ep.port 0us && U8.eq ep.net.prefix 0uy && address_is_null ep.net.addr diff --git a/collector/verified/tests/CMakeLists.txt b/collector/verified/tests/CMakeLists.txt new file mode 100644 index 0000000000..7557d889d1 --- /dev/null +++ b/collector/verified/tests/CMakeLists.txt @@ -0,0 +1,13 @@ +include(FetchContent) +FetchContent_Declare(rapidcheck + GIT_REPOSITORY https://github.com/emil-e/rapidcheck.git + GIT_TAG c60b8ec) +FetchContent_MakeAvailable(rapidcheck) + +add_executable(test_verified_network test_network.cpp) +target_link_libraries(test_verified_network collector_lib verified rapidcheck) +add_test(NAME test_verified_network COMMAND test_verified_network) + +add_executable(test_verified_nradix test_nradix.cpp) +target_link_libraries(test_verified_nradix collector_lib verified rapidcheck) +add_test(NAME test_verified_nradix COMMAND test_verified_nradix) diff --git a/collector/verified/tests/test_network.cpp b/collector/verified/tests/test_network.cpp new file mode 100644 index 0000000000..000f6df46e --- /dev/null +++ b/collector/verified/tests/test_network.cpp @@ -0,0 +1,101 @@ +#include +#include +#include + +#include + +#include "NetworkConnection.h" + +extern "C" { +#include "extracted/NetworkOps.h" +} + +// --- Conversion helpers --- + +NetworkTypes_address to_verified(const collector::Address& addr) { + NetworkTypes_address va; + va.hi = addr.array()[0]; + va.lo = addr.array()[1]; + switch (addr.family()) { + case collector::Address::Family::IPV4: + va.family = NetworkTypes_FamilyIPv4; + break; + case collector::Address::Family::IPV6: + va.family = NetworkTypes_FamilyIPv6; + break; + default: + va.family = NetworkTypes_FamilyUnknown; + break; + } + return va; +} + +// --- RapidCheck generators --- + +namespace rc { + +template<> +struct Arbitrary { + static Gen arbitrary() { + return gen::oneOf( + // Random IPv4 + gen::map(gen::arbitrary(), [](uint32_t v) { + return collector::Address(htonl(v)); + }), + // Random IPv6 + gen::map( + gen::pair(gen::arbitrary(), gen::arbitrary()), + [](std::pair v) { + return collector::Address(v.first, v.second); + } + ), + // Edge cases + gen::just(collector::Address()), + gen::just(collector::Address(127, 0, 0, 1)), + gen::just(collector::Address(0ULL, htobe64(1ULL))), + gen::just(collector::Address(10, 0, 0, 1)), + gen::just(collector::Address(8, 8, 8, 8)), + gen::just(collector::Address(255, 255, 255, 255)), + gen::just(collector::Address(192, 168, 1, 1)), + gen::just(collector::Address(172, 16, 0, 1)) + ); + } +}; + +} // namespace rc + +// --- Tests --- + +int main() { + int failures = 0; + + auto check = [&](const char* name, auto prop) { + auto result = rc::check(name, prop); + if (!result) failures++; + }; + + check("IsLocal agrees", [](collector::Address addr) { + auto va = to_verified(addr); + RC_ASSERT(addr.IsLocal() == NetworkOps_address_is_local(va)); + }); + + check("IsPublic agrees", [](collector::Address addr) { + auto va = to_verified(addr); + RC_ASSERT(addr.IsPublic() == NetworkOps_address_is_public(va)); + }); + + check("IsEphemeralPort agrees", [](uint16_t port) { + int cpp_result = collector::IsEphemeralPort(port); + uint8_t verified_result = NetworkOps_is_ephemeral_port(port); + RC_ASSERT(cpp_result == static_cast(verified_result)); + }); + + check("IsCanonicalExternalIp agrees", [](collector::Address addr) { + auto va = to_verified(addr); + RC_ASSERT(collector::Address::IsCanonicalExternalIp(addr) == + NetworkOps_is_canonical_external(va)); + }); + + printf("\n=== Results: %d failures ===\n", failures); + return failures; +} diff --git a/collector/verified/tests/test_nradix.cpp b/collector/verified/tests/test_nradix.cpp new file mode 100644 index 0000000000..6f64c1bc5e --- /dev/null +++ b/collector/verified/tests/test_nradix.cpp @@ -0,0 +1,177 @@ +#include +#include +#include + +#include + +#include "NetworkConnection.h" +#include "NRadix.h" + +extern "C" { +#include "extracted/NRadixPulse.h" +#include "extracted/internal/NetworkTypes.h" +} + +// --- Conversion helpers --- + +static NetworkTypes_address to_verified_addr(const collector::Address& addr) { + NetworkTypes_address va; + va.hi = addr.array()[0]; + va.lo = addr.array()[1]; + switch (addr.family()) { + case collector::Address::Family::IPV4: + va.family = NetworkTypes_FamilyIPv4; + break; + case collector::Address::Family::IPV6: + va.family = NetworkTypes_FamilyIPv6; + break; + default: + va.family = NetworkTypes_FamilyUnknown; + break; + } + return va; +} + +static NetworkTypes_ipnet to_verified_ipnet(const collector::IPNet& net) { + auto va = to_verified_addr(net.address()); + return NetworkTypes_mk_ipnet(va, static_cast(net.bits())); +} + +// --- RapidCheck generators --- + +namespace rc { + +template<> +struct Arbitrary { + static Gen arbitrary() { + return gen::oneOf( + gen::map(gen::arbitrary(), [](uint32_t v) { + return collector::Address(htonl(v)); + }), + gen::map( + gen::pair(gen::arbitrary(), gen::arbitrary()), + [](std::pair v) { + return collector::Address(v.first, v.second); + } + ), + gen::just(collector::Address(127, 0, 0, 1)), + gen::just(collector::Address(10, 0, 0, 1)), + gen::just(collector::Address(192, 168, 1, 1)), + gen::just(collector::Address(172, 16, 0, 1)), + gen::just(collector::Address(8, 8, 8, 8)), + gen::just(collector::Address(255, 255, 255, 255)) + ); + } +}; + +template<> +struct Arbitrary { + static Gen arbitrary() { + return gen::oneOf( + gen::map( + gen::pair(gen::arbitrary(), gen::inRange(1, 33)), + [](std::pair v) { + return collector::IPNet(collector::Address(htonl(v.first)), v.second); + } + ), + gen::map( + gen::tuple(gen::arbitrary(), gen::arbitrary(), + gen::inRange(1, 129)), + [](std::tuple v) { + return collector::IPNet( + collector::Address(std::get<0>(v), std::get<1>(v)), + std::get<2>(v)); + } + ), + gen::just(collector::IPNet(collector::Address(10, 0, 0, 0), 8)), + gen::just(collector::IPNet(collector::Address(192, 168, 0, 0), 16)), + gen::just(collector::IPNet(collector::Address(172, 16, 0, 0), 12)) + ); + } +}; + +} // namespace rc + +// --- Tests --- + +int main() { + int failures = 0; + + auto check = [&](const char* name, auto prop) { + auto result = rc::check(name, prop); + if (!result) failures++; + }; + + // --- Public API property tests --- + + check("Empty tree is empty", []() { + collector::NRadixTree tree; + RC_ASSERT(tree.IsEmpty()); + }); + + check("Insert makes tree non-empty", [](collector::IPNet net) { + RC_PRE(!net.IsNull() && net.bits() >= 1u && net.bits() <= 128u); + collector::NRadixTree tree; + tree.Insert(net); + RC_ASSERT(!tree.IsEmpty()); + }); + + check("Find after insert returns a containing network", [](collector::IPNet net) { + RC_PRE(!net.IsNull() && net.bits() >= 1u && net.bits() <= 128u); + collector::NRadixTree tree; + tree.Insert(net); + auto result = tree.Find(net.address()); + RC_ASSERT(!result.IsNull()); + RC_ASSERT(result.Contains(net.address())); + }); + + check("Find on empty tree returns null", [](collector::Address addr) { + collector::NRadixTree tree; + auto result = tree.Find(addr); + RC_ASSERT(result.IsNull()); + }); + + check("GetAll returns all inserted networks", []() { + auto nets = *rc::gen::container>( + rc::gen::arbitrary()); + collector::NRadixTree tree; + size_t count = 0; + for (const auto& net : nets) { + if (!net.IsNull() && net.bits() >= 1u && net.bits() <= 128u) { + if (tree.Insert(net)) count++; + } + } + auto all = tree.GetAll(); + RC_ASSERT(all.size() == count); + }); + + // --- Raw verified API tests --- + + check("Verified: empty tree find returns not-found", [](collector::Address addr) { + NRadixPulse_nradix_tree tree = NRadixPulse_create(); + auto va = to_verified_addr(addr); + auto result = NRadixPulse_find_addr(tree, va); + RC_ASSERT(!result.found); + NRadixPulse_destroy(tree); + }); + + check("Verified: insert then find succeeds", [](collector::IPNet net) { + RC_PRE(!net.IsNull() && net.bits() >= 1u && net.bits() <= 128u); + NRadixPulse_nradix_tree tree = NRadixPulse_create(); + tree = NRadixPulse_insert(tree, to_verified_ipnet(net)); + auto va = to_verified_addr(net.address()); + auto result = NRadixPulse_find_addr(tree, va); + RC_ASSERT(result.found); + RC_ASSERT(result.net.prefix == static_cast(net.bits())); + NRadixPulse_destroy(tree); + }); + + check("Verified: is_empty on fresh tree", []() { + NRadixPulse_nradix_tree tree = NRadixPulse_create(); + RC_ASSERT(NRadixPulse_is_empty(tree)); + NRadixPulse_destroy(tree); + }); + + printf("\n=== Results: %d failures ===\n", failures); + return failures; +}