From aacada90ff7585e65b65e3c3b3c9d6599ef77c27 Mon Sep 17 00:00:00 2001 From: Zhengyao Lin Date: Fri, 27 Jun 2025 15:37:53 -0400 Subject: [PATCH] Update to use the official Verus repo --- .github/workflows/build.yml | 31 ++++++++++++++++---- .gitmodules | 2 +- README.md | 13 ++++----- deps/verus | 2 +- deps/vest/src/regular/repeat.rs | 2 ++ deps/vest/src/utils.rs | 2 ++ rust-toolchain.toml | 2 +- tools/activate.sh | 19 ------------ verdict-bin/Cargo.toml | 1 + verdict-parser/Cargo.toml | 4 +++ verdict-parser/src/asn1/base128.rs | 12 +++++--- verdict-parser/src/asn1/bounds.rs | 2 ++ verdict-parser/src/asn1/var_int.rs | 2 ++ verdict-parser/src/common/base64.rs | 2 ++ verdict-parser/src/common/repeat.rs | 4 +++ verdict-parser/src/common/wrapped.rs | 10 +++---- verdict-parser/src/x509/oid.rs | 2 +- verdict-polyfill/src/lib.rs | 11 +++---- verdict-rspec/src/lib.rs | 4 +-- verdict/Cargo.toml | 1 + verdict/src/convert.rs | 2 +- verdict/src/hash.rs | 8 +++--- verdict/src/issue.rs | 7 ++--- verdict/src/policy/chrome.rs | 14 ++++----- verdict/src/policy/common.rs | 10 +++---- verdict/src/policy/firefox.rs | 14 ++++----- verdict/src/policy/openssl.rs | 14 ++++----- verdict/src/policy/standard.rs | 40 +++++++++++++------------- verdict/src/signature/ecdsa_aws_lc.rs | 8 +++--- verdict/src/signature/ecdsa_libcrux.rs | 4 +-- verdict/src/signature/rsa_aws_lc.rs | 6 ++-- verdict/src/signature/rsa_libcrux.rs | 4 +-- verdict/src/validator.rs | 12 ++++---- 33 files changed, 146 insertions(+), 125 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 35d6e95..43eccd6 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -10,7 +10,7 @@ env: CARGO_TERM_COLOR: always jobs: - build: + verified-build: runs-on: ubuntu-latest steps: @@ -18,9 +18,28 @@ jobs: uses: actions/checkout@v4 with: submodules: true - - name: Build Debug - run: source tools/activate.sh && vargo build - - name: Build Release - run: source tools/activate.sh && vargo build --release + - name: Build debug + run: source tools/activate.sh && cargo verus build + - name: Build debug with tracing + run: source tools/activate.sh && cargo verus build --features trace + - name: Build release + run: source tools/activate.sh && cargo verus build --release + - name: Build release with aws-lc feature + run: source tools/activate.sh && cargo verus build --release --features aws-lc - name: Test - run: source tools/activate.sh && vargo test --workspace + run: source tools/activate.sh && cargo test --workspace + + unverified-build: + runs-on: ubuntu-latest + + steps: + - name: Checkout + uses: actions/checkout@v4 + with: + submodules: true + - name: Build debug + run: cargo build + - name: Build release + run: cargo build --release + - name: Build release with aws-lc feature + run: cargo build --release --features aws-lc diff --git a/.gitmodules b/.gitmodules index 71154b0..367fa77 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,6 @@ [submodule "deps/verus"] path = deps/verus - url = https://github.com/zhengyao-lin/verus.git + url = https://github.com/verus-lang/verus.git branch = x509 [submodule "deps/libcrux"] path = deps/libcrux diff --git a/README.md b/README.md index 3a9830e..420f865 100644 --- a/README.md +++ b/README.md @@ -18,26 +18,25 @@ To build, first run (Bash or Zsh) ``` . tools/activate.sh ``` -This will first compile a vendored version of Verus, and then -provide a command `vargo` with the same usage as `cargo`. +This will first compile a vendored version of Verus and add relevant binaries to `PATH`. To verify and build the entire project, run ``` -vargo build --release +cargo verus build --release ``` Then use `target/release/verdict` to validate certificate chains or run benchmarks. See `target/release/verdict --help` for details. -By default, we only use crypto primitives that are verified from [libcrux](https://github.com/cryspen/libcrux) and [aws-lc-rs](https://github.com/aws/aws-lc-rs). +By default, we only use *verified* crypto primitives from [libcrux](https://github.com/cryspen/libcrux) and [aws-lc-rs](https://github.com/aws/aws-lc-rs). To use primitives entirely from `aws-lc-rs` which might have better performance but include unverified signature checking for RSA and ECDSA P-256, compile with ``` -vargo build --release --features aws-lc +cargo verus build --release --features aws-lc ``` To run some sanity checks ``` -vargo test --workspace +cargo test --workspace ``` ### Build without verification @@ -56,7 +55,7 @@ which should work like in a normal Rust package, with all verification annotatio Use ``` -RUSTFLAGS="--cfg trace" vargo build [--release] +cargo verus build [--release] --features trace ``` to build a version with tracing enabled. This will print out every successfully parsed construct and the result of each predicate in the policy DSL. diff --git a/deps/verus b/deps/verus index 8e09669..112ecd1 160000 --- a/deps/verus +++ b/deps/verus @@ -1 +1 @@ -Subproject commit 8e096695ccd42aaac479201c101030ca8532a1de +Subproject commit 112ecd1c1607ef8715a6bc66259e1dd7fd29c245 diff --git a/deps/vest/src/regular/repeat.rs b/deps/vest/src/regular/repeat.rs index b9ed17f..0c96a8b 100644 --- a/deps/vest/src/regular/repeat.rs +++ b/deps/vest/src/regular/repeat.rs @@ -202,6 +202,7 @@ impl Repeat where }, offset < s@.len() ==> (self@.spec_parse(s@.subrange(offset as int, s@.len() as int)) is Err ==> self@.spec_parse(s@) is Err), + decreases s.len() - offset { let (n, v) = self.0.parse(slice_subrange(s, offset, s.len()))?; if n == 0 { @@ -240,6 +241,7 @@ impl Repeat where &&& self@.spec_serialize(old(v)@) matches Ok(s) ==> n == (len + s.len()) && data@ =~= seq_splice(old(data)@, (pos + len) as usize, s) }, + decreases old(v)@.len() { if pos > usize::MAX - len || pos + len >= data.len() { return Err(SerializeError::InsufficientBuffer); diff --git a/deps/vest/src/utils.rs b/deps/vest/src/utils.rs index b1316b3..603ef58 100644 --- a/deps/vest/src/utils.rs +++ b/deps/vest/src/utils.rs @@ -194,6 +194,7 @@ pub fn set_range<'a>(data: &mut Vec, i: usize, input: &[u8]) forall|k| i + input@.len() <= k < data@.len() ==> data@[k] == old(data)@[k], 0 <= i <= i + j <= i + input@.len() <= data@.len() <= usize::MAX, forall|k| 0 <= k < j ==> data@[i + k] == input@[k], + decreases input.len() - j { data.set(i + j, *slice_index_get(input, j)); j = j + 1 @@ -249,6 +250,7 @@ pub exec fn init_vec_u8(n: usize) -> (res: Vec) invariant 0 <= i <= n, ret@.len() == i, + decreases n - i { ret.push(0); assert(ret@[i as int] == 0); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 2e2b8c8..cf6d0f5 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,2 +1,2 @@ [toolchain] -channel = "1.82.0" +channel = "1.86.0" diff --git a/tools/activate.sh b/tools/activate.sh index 4f19ca0..7430eea 100755 --- a/tools/activate.sh +++ b/tools/activate.sh @@ -1,13 +1,6 @@ # Usage: source this script at the root of the repo -# Similar to how Verus's internal vargo would work -# https://github.com/verus-lang/verus/blob/main/tools/activate - -unset -f cargo 2>/dev/null || true -unset -f vargo 2>/dev/null || true - REPO_ROOT=$(pwd) -REAL_CARGO="$(which cargo)" git submodule update --init @@ -18,16 +11,4 @@ rustup toolchain install && source ../tools/activate && vargo build --release) || return 1 -# Build verusc -(cd "tools/verusc" && cargo build --release) || return 1 - -vargo() { - RUSTC_WRAPPER="$REPO_ROOT/tools/verusc/target/release/verusc" "$REAL_CARGO" "$@" -} - -cargo() { - echo You have activated the build environment of Verus, so it is likely that - echo you want to use \`vargo\` instead of \`cargo\`. Restart the shell to disable. -} - export PATH="$REPO_ROOT/deps/verus/source/target-verus/release:$PATH" diff --git a/verdict-bin/Cargo.toml b/verdict-bin/Cargo.toml index e40ecb1..7e81203 100644 --- a/verdict-bin/Cargo.toml +++ b/verdict-bin/Cargo.toml @@ -24,3 +24,4 @@ rand = "0.8.5" [features] default = [] aws-lc = ["verdict/aws-lc"] +trace = ["verdict/trace"] diff --git a/verdict-parser/Cargo.toml b/verdict-parser/Cargo.toml index e7f1518..38a5136 100644 --- a/verdict-parser/Cargo.toml +++ b/verdict-parser/Cargo.toml @@ -14,6 +14,10 @@ der = { version = "0.7.9", features = [ "alloc", "oid" ] } base64 = "0.22.1" paste = "1.0.15" +[features] +default = [] +trace = [] + [package.metadata.verus] verify = true diff --git a/verdict-parser/src/asn1/base128.rs b/verdict-parser/src/asn1/base128.rs index 520ddea..d10c1ec 100644 --- a/verdict-parser/src/asn1/base128.rs +++ b/verdict-parser/src/asn1/base128.rs @@ -118,7 +118,7 @@ impl Base128UInt { /// Serialize v in base-128 encoding /// last_byte is true iff the encoding should have the highest bit of the last byte set to 0 closed spec fn spec_serialize_helper(v: UInt, last_byte: bool) -> Seq - decreases v via Self::spec_serialize_dereases + decreases v via Self::spec_serialize_decreases { if v == 0 { if last_byte { @@ -289,8 +289,7 @@ impl Base128UInt { } #[via_fn] - proof fn spec_serialize_dereases(v: UInt, last_byte: bool) - { + proof fn spec_serialize_decreases(v: UInt, last_byte: bool) { assert(v != 0 ==> v >> 7 < v) by (bit_vector); } @@ -467,6 +466,7 @@ impl Base128UInt { invariant 0 <= len <= s.len(), Self::all_high_8_bit_set(s@.take(len as int)), + decreases s.len() - len { len = len + 1; @@ -512,13 +512,15 @@ impl Base128UInt { /// TODO: change this to a non-recursive function #[inline(always)] - fn serialize_helper(v: UInt) -> (r: Vec) + fn serialize_helper(v: u64) -> (r: Vec) ensures r@ == Self::spec_serialize_helper(v, false) + decreases v { if v == 0 { Vec::with_capacity(4) // usually OID arcs fit in 4 bytes } else { // Add the lowest 7 bits with the highest bit set to 0 + assert(v != 0 ==> v >> 7 < v) by (bit_vector); let mut r = Self::serialize_helper(v >> 7); let ghost old_r = r@; @@ -591,6 +593,8 @@ impl Combinator for Base128UInt { !Self::is_high_8_bit_set(s@[len - 1]), Self::spec_parse_helper(s@.take(i as int), false).is_some(), v == Self::spec_parse_helper(s@.take(i as int), false).unwrap(), + + decreases len - 1 - i { assert(s@.take(i + 1).drop_last() == s@.take(i as int)); assert(Self::is_high_8_bit_set(s@.take(len - 1)[i as int])); diff --git a/verdict-parser/src/asn1/bounds.rs b/verdict-parser/src/asn1/bounds.rs index 61355af..b47f41e 100644 --- a/verdict-parser/src/asn1/bounds.rs +++ b/verdict-parser/src/asn1/bounds.rs @@ -262,6 +262,7 @@ pub fn min_num_bytes_unsigned_exec(v: UInt) -> (res: UInt) invariant 0 <= n <= uint_size!(), fits_n_bytes_unsigned!(v, n), + decreases n { if !fits_n_bytes_unsigned!(v, n - 1) { return n; @@ -286,6 +287,7 @@ pub fn min_num_bytes_signed_exec(v: Int) -> (res: UInt) invariant 0 <= n <= uint_size!(), fits_n_bytes_signed!(v, n), + decreases n { if !fits_n_bytes_signed!(v, n - 1) { assert(v == 0 && !fits_n_bytes_signed!(v, n - 1) ==> n == 1) by (bit_vector); diff --git a/verdict-parser/src/asn1/var_int.rs b/verdict-parser/src/asn1/var_int.rs index 4e1ac09..dff3b98 100644 --- a/verdict-parser/src/asn1/var_int.rs +++ b/verdict-parser/src/asn1/var_int.rs @@ -280,6 +280,7 @@ impl Combinator for VarUInt { // At each iteration, res is the parse result of a suffix of s res == Self((len - i) as usize).spec_parse(s@.skip(i as int)).unwrap().1, + decreases i { let byte = s[i - 1]; @@ -359,6 +360,7 @@ impl Combinator for VarUInt { (pos + i) as usize, Self((len - i) as usize).spec_serialize(v & n_byte_max_unsigned!(len - i)).unwrap(), ), + decreases i { let byte = get_nth_byte!(v, len - i); diff --git a/verdict-parser/src/common/base64.rs b/verdict-parser/src/common/base64.rs index 241d4cc..2bf2939 100644 --- a/verdict-parser/src/common/base64.rs +++ b/verdict-parser/src/common/base64.rs @@ -380,6 +380,7 @@ impl Combinator for Base64 { Self::spec_parse_helper(s@.skip(i as int)) is Err ==> Self::spec_parse_helper(s@) is Err, + decreases len - i { assert(len - i == s@.skip(i as int).len()); @@ -458,6 +459,7 @@ impl Combinator for Base64 { // Self::spec_serialize_helper(v@.skip(i as int)) is Err ==> // Self::spec_serialize_helper(v@) is Err, + decreases len - i { let v1 = v[i]; let v2 = if len - i > 1 { v[i + 1] } else { 0 }; diff --git a/verdict-parser/src/common/repeat.rs b/verdict-parser/src/common/repeat.rs index 9db6efc..3cfcc6a 100644 --- a/verdict-parser/src/common/repeat.rs +++ b/verdict-parser/src/common/repeat.rs @@ -158,6 +158,8 @@ impl Repeat where res@ =~= old(res)@ + v }, r is Err ==> self@.spec_parse(s@) is Err + + decreases s.len(), { if s.len() == 0 { return Ok(()); @@ -187,6 +189,8 @@ impl Repeat where &&& self@.spec_serialize(old(v)@) matches Ok(s) ==> n == (len + s.len()) && data@ =~= seq_splice(old(data)@, (pos + len) as usize, s) }, + + decreases old(v)@.len() { if pos > usize::MAX - len || pos + len >= data.len() { return Err(SerializeError::InsufficientBuffer); diff --git a/verdict-parser/src/common/wrapped.rs b/verdict-parser/src/common/wrapped.rs index e2446dd..2913d24 100644 --- a/verdict-parser/src/common/wrapped.rs +++ b/verdict-parser/src/common/wrapped.rs @@ -176,14 +176,14 @@ macro_rules! wrap_combinator_impls { type SpecResult = $spec_result; // $inner_expr.view().spec_parse(s) - closed spec fn spec_parse(&self, s: Seq) -> Result<(usize, Self::SpecResult), ()>; + uninterp spec fn spec_parse(&self, s: Seq) -> Result<(usize, Self::SpecResult), ()>; // $inner_expr.view().spec_parse_wf(s) #[verifier::external_body] proof fn spec_parse_wf(&self, s: Seq) {} // $inner_expr.view().spec_serialize(v) - closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result, ()>; + uninterp spec fn spec_serialize(&self, v: Self::SpecResult) -> Result, ()>; } impl SecureSpecCombinator for $name { @@ -212,7 +212,7 @@ macro_rules! wrap_combinator_impls { type Result<$lt> = $result; type Owned = $owned; - closed spec fn spec_length(&self) -> Option; + uninterp spec fn spec_length(&self) -> Option; #[verifier::external_body] fn length(&self) -> Option { @@ -230,8 +230,8 @@ macro_rules! wrap_combinator_impls { fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) { $(let $field_name: $field_type = self.$field_name;)* let res = $inner_expr.parse(s); - #[cfg(trace)] { - use polyfill::*; + #[cfg(feature = "trace")] { + use verdict_polyfill::*; eprintln_join!("[", stringify!($name), "] ", format_dbg(&res)); } res diff --git a/verdict-parser/src/x509/oid.rs b/verdict-parser/src/x509/oid.rs index d75898e..c573110 100644 --- a/verdict-parser/src/x509/oid.rs +++ b/verdict-parser/src/x509/oid.rs @@ -151,7 +151,7 @@ macro_rules! spec_oid { pub use spec_oid; /// Used to suppress Verus warning about broadcast missing triggers -pub closed spec fn lemma_disjoint_trigger() -> bool; +pub uninterp spec fn lemma_disjoint_trigger() -> bool; /// Macro to generate a lemma that states the disjointness of a list of spec terms /// NOTE: the disjointness of the provided terms are trusted diff --git a/verdict-polyfill/src/lib.rs b/verdict-polyfill/src/lib.rs index f2b84c2..cf80541 100644 --- a/verdict-polyfill/src/lib.rs +++ b/verdict-polyfill/src/lib.rs @@ -161,8 +161,8 @@ pub fn result_or(result: Result, default: Result) -> (res /// Currently we do not have a specification in Verus for UTF-8 /// so we just assume the implementation of `from_utf8` is correct -pub closed spec fn spec_parse_utf8(s: Seq) -> Option>; -pub closed spec fn spec_serialize_utf8(s: Seq) -> Seq; +pub uninterp spec fn spec_parse_utf8(s: Seq) -> Option>; +pub uninterp spec fn spec_serialize_utf8(s: Seq) -> Seq; #[verifier::external_body] pub proof fn spec_utf8_parse_serialize_roundtrip(buf: Seq) @@ -191,7 +191,7 @@ pub fn str_to_utf8(s: &str) -> (res: &[u8]) } /// We trust the implementation of `u64::to_string` for now -pub closed spec fn spec_u64_to_string(x: u64) -> (res: Seq); +pub uninterp spec fn spec_u64_to_string(x: u64) -> (res: Seq); #[verifier::external_body] pub fn char_to_string(c: char) -> (res: String) @@ -233,6 +233,7 @@ pub fn vec_map(v: &Vec, f: impl Fn(&T) -> U) -> (res: Vec) 0 <= j <= v.len(), j == res.len(), forall|i| #![trigger v[i]] 0 <= i < j ==> call_ensures(f, (&v[i],), #[trigger] res[i]), + decreases v.len() - j { res.push(f(&v[j])); j += 1; @@ -509,8 +510,8 @@ pub fn eprintln_debug(s: T) { #[verifier::external_body] pub struct CharsIter<'a>(std::str::Chars<'a>); -pub closed spec fn spec_chars_iter_str<'a>(iter: CharsIter<'a>) -> Seq; -pub closed spec fn spec_chars_iter_index<'a>(iter: CharsIter<'a>) -> int; +pub uninterp spec fn spec_chars_iter_str<'a>(iter: CharsIter<'a>) -> Seq; +pub uninterp spec fn spec_chars_iter_index<'a>(iter: CharsIter<'a>) -> int; #[verifier::external_body] pub fn chars_iter_next<'a>(iter: &mut CharsIter<'a>) -> (res: Option) diff --git a/verdict-rspec/src/lib.rs b/verdict-rspec/src/lib.rs index 2e9f369..ee40e16 100644 --- a/verdict-rspec/src/lib.rs +++ b/verdict-rspec/src/lib.rs @@ -721,7 +721,7 @@ fn get_guarded_quantifier(closure: &ExprClosure, is_forall: bool) -> Result Result { // For each function, generate an exec version for item_fn in ctx.fns.values() { let exec_fn = compile_spec_fn(&ctx, item_fn, trace)?; - output.push(quote! { #[verifier::loop_isolation(false)] #exec_fn }); + output.push(quote! { #[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] #exec_fn }); } // println!("########################################"); diff --git a/verdict/Cargo.toml b/verdict/Cargo.toml index 482906c..9d8b7ad 100644 --- a/verdict/Cargo.toml +++ b/verdict/Cargo.toml @@ -21,6 +21,7 @@ verdict-rspec-lib = { path = "../verdict-rspec-lib" } [features] default = [] aws-lc = [] +trace = ["verdict-parser/trace"] [package.metadata.verus] verify = true diff --git a/verdict/src/convert.rs b/verdict/src/convert.rs index 00fd416..05faef9 100644 --- a/verdict/src/convert.rs +++ b/verdict/src/convert.rs @@ -332,7 +332,7 @@ impl policy::Certificate { res } - pub closed spec fn spec_time_to_timestamp(time: SpecTimeValue) -> Option; + pub uninterp spec fn spec_time_to_timestamp(time: SpecTimeValue) -> Option; /// Convert an X.509 Time to a UNIX timestamp /// NOTE: this implementation is unverified and trusted diff --git a/verdict/src/hash.rs b/verdict/src/hash.rs index be8360e..1fdefa5 100644 --- a/verdict/src/hash.rs +++ b/verdict/src/hash.rs @@ -7,10 +7,10 @@ use libcrux::digest; verus! { -pub closed spec fn spec_sha224_digest(data: Seq) -> Seq; -pub closed spec fn spec_sha256_digest(data: Seq) -> Seq; -pub closed spec fn spec_sha384_digest(data: Seq) -> Seq; -pub closed spec fn spec_sha512_digest(data: Seq) -> Seq; +pub uninterp spec fn spec_sha224_digest(data: Seq) -> Seq; +pub uninterp spec fn spec_sha256_digest(data: Seq) -> Seq; +pub uninterp spec fn spec_sha384_digest(data: Seq) -> Seq; +pub uninterp spec fn spec_sha512_digest(data: Seq) -> Seq; #[verifier::external_body] #[inline(always)] diff --git a/verdict/src/issue.rs b/verdict/src/issue.rs index 9c9c27c..5174d47 100644 --- a/verdict/src/issue.rs +++ b/verdict/src/issue.rs @@ -135,9 +135,8 @@ pub fn normalize_string(s: &str) -> (res: String) i == spec_chars_iter_index(iter), spec_normalize_string(s@) =~= res@ + spec_normalize_string_helper(s@.skip(i as int), seen_nw, seen_ws), - - ensures - i == s@.len(), + ensures i == s@.len() + decreases s@.len() - i { if let Some(c) = chars_iter_next(&mut iter) { if c == ' ' { @@ -165,7 +164,7 @@ pub fn normalize_string(s: &str) -> (res: String) } /// NOTE: For lower case folding, we trust Rust's built-in definition -pub closed spec fn spec_char_lower(c: char) -> Seq; +pub uninterp spec fn spec_char_lower(c: char) -> Seq; #[verifier::external_body] #[inline(always)] diff --git a/verdict/src/policy/chrome.rs b/verdict/src/policy/chrome.rs index c1d892c..692d64c 100644 --- a/verdict/src/policy/chrome.rs +++ b/verdict/src/policy/chrome.rs @@ -4,8 +4,8 @@ use vstd::prelude::*; use verdict_polyfill::strs_to_strings; -#[cfg(trace)] use verdict_rspec::rspec_trace as rspec; -#[cfg(not(trace))] use verdict_rspec::rspec; +#[cfg(feature = "trace")] use verdict_rspec::rspec_trace as rspec; +#[cfg(not(feature = "trace"))] use verdict_rspec::rspec; use verdict_rspec_lib::*; use super::common::*; @@ -23,11 +23,11 @@ impl Policy for ChromePolicy { internal::exec_likely_issued(issuer, subject) } - closed spec fn spec_valid_chain(&self, chain: Seq, task: Task) -> Result { + closed spec fn spec_valid_chain(&self, chain: Seq, task: Task) -> bool { internal::valid_chain(&self.deep_view(), &chain, &task) } - fn valid_chain(&self, chain: &Vec<&ExecCertificate>, task: &ExecTask) -> Result { + fn valid_chain(&self, chain: &Vec<&ExecCertificate>, task: &ExecTask) -> bool { internal::exec_valid_chain(self, chain, task) } } @@ -576,9 +576,9 @@ pub open spec fn check_all_name_constraints(chain: &Seq>) - /// chain[0] is the leaf, and assume chain[i] is issued by chain[i + 1] for all i < chain.len() - 1 /// chain.last() must be a trusted root -pub open spec fn valid_chain(env: &Policy, chain: &Seq>, task: &Task) -> Result +pub open spec fn valid_chain(env: &Policy, chain: &Seq>, task: &Task) -> bool { - Ok(chain.len() >= 2 && { + chain.len() >= 2 && { let leaf = &chain[0]; let root = &chain[chain.len() - 1]; @@ -586,7 +586,7 @@ pub open spec fn valid_chain(env: &Policy, chain: &Seq>, ta &&& forall |i: usize| 1 <= i < chain.len() - 1 ==> cert_verified_intermediate(&env, &task, #[trigger] &chain[i as int], (i - 1) as usize) &&& cert_verified_root(env, task, root, &chain[chain.len() - 2], (chain.len() - 2) as usize) &&& check_all_name_constraints(chain) - }) + } } pub open spec fn likely_issued(issuer: &Certificate, subject: &Certificate) -> bool diff --git a/verdict/src/policy/common.rs b/verdict/src/policy/common.rs index 049ca7e..4f842b5 100644 --- a/verdict/src/policy/common.rs +++ b/verdict/src/policy/common.rs @@ -2,8 +2,8 @@ #![allow(unexpected_cfgs)] use vstd::prelude::*; -#[cfg(trace)] use verdict_rspec::rspec_trace as rspec; -#[cfg(not(trace))] use verdict_rspec::rspec; +#[cfg(feature = "trace")] use verdict_rspec::rspec_trace as rspec; +#[cfg(not(feature = "trace"))] use verdict_rspec::rspec; use verdict_rspec_lib::*; use crate::issue; @@ -21,9 +21,9 @@ pub trait Policy: Send + Sync { ensures res == self.spec_likely_issued(issuer.deep_view(), subject.deep_view()); /// User-defined chain/path validation - spec fn spec_valid_chain(&self, chain: Seq, task: Task) -> Result; + spec fn spec_valid_chain(&self, chain: Seq, task: Task) -> bool; - fn valid_chain(&self, chain: &Vec<&ExecCertificate>, task: &ExecTask) -> (res: Result) + fn valid_chain(&self, chain: &Vec<&ExecCertificate>, task: &ExecTask) -> (res: bool) ensures res.deep_view() == self.spec_valid_chain(chain.deep_view(), task.deep_view()); } @@ -358,7 +358,7 @@ pub open spec fn check_duplicate_extensions(cert: &Certificate) -> bool } // rspec! /// NOTE: unspecified -pub closed spec fn str_lower(s: &SpecString) -> SpecString; +pub uninterp spec fn str_lower(s: &SpecString) -> SpecString; #[verifier::external_body] pub fn exec_str_lower(s: &String) -> (res: String) diff --git a/verdict/src/policy/firefox.rs b/verdict/src/policy/firefox.rs index bbe40a7..3fe6fdb 100644 --- a/verdict/src/policy/firefox.rs +++ b/verdict/src/policy/firefox.rs @@ -5,8 +5,8 @@ use vstd::prelude::*; use verdict_polyfill::strs_to_strings; -#[cfg(trace)] use verdict_rspec::rspec_trace as rspec; -#[cfg(not(trace))] use verdict_rspec::rspec; +#[cfg(feature = "trace")] use verdict_rspec::rspec_trace as rspec; +#[cfg(not(feature = "trace"))] use verdict_rspec::rspec; use verdict_rspec_lib::*; use super::common::*; @@ -24,11 +24,11 @@ impl Policy for FirefoxPolicy { internal::exec_likely_issued(issuer, subject) } - closed spec fn spec_valid_chain(&self, chain: Seq, task: Task) -> Result { + closed spec fn spec_valid_chain(&self, chain: Seq, task: Task) -> bool { internal::valid_chain(&self.deep_view(), &chain, &task) } - fn valid_chain(&self, chain: &Vec<&ExecCertificate>, task: &ExecTask) -> Result { + fn valid_chain(&self, chain: &Vec<&ExecCertificate>, task: &ExecTask) -> bool { internal::exec_valid_chain(self, chain, task) } } @@ -619,9 +619,9 @@ pub open spec fn check_all_name_constraints(chain: &Seq>) - /// chain[0] is the leaf, and assume chain[i] is issued by chain[i + 1] for all i < chain.len() - 1 /// chain.last() must be a trusted root -pub open spec fn valid_chain(env: &Policy, chain: &Seq>, task: &Task) -> Result +pub open spec fn valid_chain(env: &Policy, chain: &Seq>, task: &Task) -> bool { - Ok(chain.len() >= 2 && { + chain.len() >= 2 && { let leaf = &chain[0]; let root = &chain[chain.len() - 1]; @@ -629,7 +629,7 @@ pub open spec fn valid_chain(env: &Policy, chain: &Seq>, ta &&& forall |i: usize| 1 <= i < chain.len() - 1 ==> cert_verified_intermediate(&env, &task, #[trigger] &chain[i as int], &leaf, (i - 1) as usize) &&& cert_verified_root(env, task, root, &chain[chain.len() - 2], leaf, (chain.len() - 2) as usize) &&& check_all_name_constraints(chain) - }) + } } pub open spec fn likely_issued(issuer: &Certificate, subject: &Certificate) -> bool diff --git a/verdict/src/policy/openssl.rs b/verdict/src/policy/openssl.rs index 6b5737e..72c8a5e 100644 --- a/verdict/src/policy/openssl.rs +++ b/verdict/src/policy/openssl.rs @@ -2,8 +2,8 @@ #![allow(unexpected_cfgs)] use vstd::prelude::*; -#[cfg(trace)] use verdict_rspec::rspec_trace as rspec; -#[cfg(not(trace))] use verdict_rspec::rspec; +#[cfg(feature = "trace")] use verdict_rspec::rspec_trace as rspec; +#[cfg(not(feature = "trace"))] use verdict_rspec::rspec; use verdict_rspec_lib::*; use super::common::*; @@ -21,11 +21,11 @@ impl Policy for OpenSSLPolicy { internal::exec_likely_issued(issuer, subject) } - closed spec fn spec_valid_chain(&self, chain: Seq, task: Task) -> Result { + closed spec fn spec_valid_chain(&self, chain: Seq, task: Task) -> bool { internal::valid_chain(&self.deep_view(), &chain, &task) } - fn valid_chain(&self, chain: &Vec<&ExecCertificate>, task: &ExecTask) -> Result { + fn valid_chain(&self, chain: &Vec<&ExecCertificate>, task: &ExecTask) -> bool { internal::exec_valid_chain(self, chain, task) } } @@ -524,15 +524,15 @@ pub open spec fn valid_root(env: &Policy, task: &Task, cert: &Certificate, depth /// chain[0] is the leaf, and assume chain[i] is issued by chain[i + 1] for all i < chain.len() - 1 /// chain.last() must be a trusted root -pub open spec fn valid_chain(env: &Policy, chain: &Seq>, task: &Task) -> Result +pub open spec fn valid_chain(env: &Policy, chain: &Seq>, task: &Task) -> bool { - Ok(chain.len() >= 2 && { + chain.len() >= 2 && { &&& valid_leaf(env, task, &chain[0]) &&& forall |i: usize| 1 <= i < chain.len() - 1 ==> valid_intermediate(&env, &task, #[trigger] &chain[i as int], (i - 1) as usize) &&& valid_root(env, task, &chain[chain.len() - 1], (chain.len() - 2) as usize) &&& check_name_constraints(chain) &&& &task.hostname matches Some(hostname) ==> check_hostname(&chain[0], hostname) - }) + } } pub open spec fn likely_issued(issuer: &Certificate, subject: &Certificate) -> bool diff --git a/verdict/src/policy/standard.rs b/verdict/src/policy/standard.rs index b2ce789..6045f31 100644 --- a/verdict/src/policy/standard.rs +++ b/verdict/src/policy/standard.rs @@ -9,7 +9,7 @@ verus! { /// A validated chain should not contain expired certificates pub trait NoExpiration: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 0 <= i < chain.len() ==> @@ -19,7 +19,7 @@ pub trait NoExpiration: Policy { /// Outer signature algorithm should match the inner one pub trait OuterInnerSigMatch: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 0 <= i < chain.len() ==> @@ -29,7 +29,7 @@ pub trait OuterInnerSigMatch: Policy { /// If the extension KeyUsage is present, at least one bit must be set pub trait KeyUsageNonEmpty: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 0 <= i < chain.len() ==> @@ -49,7 +49,7 @@ pub trait KeyUsageNonEmpty: Policy { /// Issuer and subject UID should only appear if version is 2 or 3 pub trait IssuerSubjectUIDVersion: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 0 <= i < chain.len() ==> @@ -61,7 +61,7 @@ pub trait IssuerSubjectUIDVersion: Policy { /// PathLenConstraints should be non-negative pub trait PathLenNonNegative: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 0 <= i < chain.len() ==> @@ -75,7 +75,7 @@ pub trait PathLenNonNegative: Policy { /// non-leaf certificates pub trait PathLenConstraint: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 1 <= i < chain.len() ==> { @@ -93,7 +93,7 @@ pub trait PathLenConstraint: Policy { /// Every non-leaf certificate must be a CA certificate pub trait NonLeafMustBeCA: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 1 <= i < chain.len() ==> @@ -103,7 +103,7 @@ pub trait NonLeafMustBeCA: Policy { /// Every non-leaf certificate must have keyCertSign set in KeyUsage (if present) pub trait NonLeafHasKeyCertSign: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 1 <= i < chain.len() ==> @@ -113,7 +113,7 @@ pub trait NonLeafHasKeyCertSign: Policy { /// If SubjectAltName is present, it should contain at least one name pub trait NonEmptySAN: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 0 <= i < chain.len() ==> @@ -124,7 +124,7 @@ pub trait NonEmptySAN: Policy { /// Conforming CAs MUST mark this (AKI) extension as non-critical. pub trait AKINonCritical: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures chain.last().ext_authority_key_id matches Some(akid) ==> !akid.critical.unwrap_or(false); @@ -136,7 +136,7 @@ pub trait AKINonCritical: Policy { /// facilitate certification path construction. pub trait NonRootHasAKI: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 0 <= i < chain.len() - 1 ==> @@ -151,7 +151,7 @@ pub trait NonRootHasAKI: Policy { /// value of cA is TRUE. pub trait NonLeafHasSKI: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 1 <= i < chain.len() ==> @@ -163,7 +163,7 @@ pub trait NonLeafHasSKI: Policy { /// include a subjectAltName extension that is marked as critical. pub trait EmptySubjectImpliesCriticalSAN: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures chain[0].subject.0.len() == 0 ==> (chain[0].ext_subject_alt_name matches Some(san) && @@ -174,7 +174,7 @@ pub trait EmptySubjectImpliesCriticalSAN: Policy { /// Conforming CAs MUST mark this extension (SKI) as non-critical. pub trait NonCriticalRootSKI: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures chain.last().ext_subject_key_id matches Some(skid) ==> !skid.critical.unwrap_or(false); @@ -185,7 +185,7 @@ pub trait NonCriticalRootSKI: Policy { /// keyIdentifier MUST be present. MUST be identical to the subjectKeyIdentifier field. pub trait RootCAHasAKI: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures chain.last().ext_authority_key_id matches Some(akid) && akid.key_id matches Some(..); @@ -197,7 +197,7 @@ pub trait RootCAHasAKI: Policy { /// authorityCertSerialNumber MUST NOT be present pub trait RootCAAKINoIssuerOrSerial: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures chain.last().ext_authority_key_id matches Some(akid) ==> akid.issuer matches None && akid.serial matches None; @@ -207,7 +207,7 @@ pub trait RootCAAKINoIssuerOrSerial: Policy { /// CA/B BR 7.1.2.7.6 pub trait LeafHasEKU: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures chain[0].ext_extended_key_usage matches Some(eku) && !eku.critical.unwrap_or(false); @@ -217,7 +217,7 @@ pub trait LeafHasEKU: Policy { /// CA/B BR 7.1.2.1.2 pub trait RootHasNoEKU: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures chain.last().ext_extended_key_usage matches None; } @@ -226,7 +226,7 @@ pub trait RootHasNoEKU: Policy { /// CA/B BR does not allow DSA keys pub trait NoDSA: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 0 <= i < chain.len() ==> @@ -238,7 +238,7 @@ pub trait NoDSA: Policy { /// - Ensure that the modulus size, when encoded, is at least 2048 bits pub trait RSA2048: Policy { proof fn conformance(&self, chain: Seq, task: Task) - requires self.spec_valid_chain(chain, task) matches Ok(res) && res + requires self.spec_valid_chain(chain, task) ensures forall |i: usize| #![trigger chain[i as int]] 0 <= i < chain.len() diff --git a/verdict/src/signature/ecdsa_aws_lc.rs b/verdict/src/signature/ecdsa_aws_lc.rs index 4ad2bae..927fdea 100644 --- a/verdict/src/signature/ecdsa_aws_lc.rs +++ b/verdict/src/signature/ecdsa_aws_lc.rs @@ -6,14 +6,14 @@ use verdict_parser::x509::*; verus! { -pub closed spec fn spec_p256_verify( +pub uninterp spec fn spec_p256_verify( alg: SpecAlgorithmIdentifierValue, pub_key: Seq, sig: Seq, msg: Seq, ) -> bool; -pub closed spec fn spec_p384_verify( +pub uninterp spec fn spec_p384_verify( alg: SpecAlgorithmIdentifierValue, pub_key: Seq, sig: Seq, @@ -29,7 +29,7 @@ pub enum ECDSAError { /// Verify ECDSA P-256 signature with SHA-256/SHA-384 through AWS-LC #[verifier::external_body] pub fn p256_verify( - alg: &AlgorithmIdentifierValue, + alg: &AlgorithmIdentifierValue<'_>, pub_key: &[u8], sig: &[u8], msg: &[u8], @@ -57,7 +57,7 @@ pub fn p256_verify( /// since only P-384 + SHA-384 is verified in AWS-LC) #[verifier::external_body] pub fn p384_verify( - alg: &AlgorithmIdentifierValue, + alg: &AlgorithmIdentifierValue<'_>, pub_key: &[u8], sig: &[u8], msg: &[u8], diff --git a/verdict/src/signature/ecdsa_libcrux.rs b/verdict/src/signature/ecdsa_libcrux.rs index 8354ecc..3adb07a 100644 --- a/verdict/src/signature/ecdsa_libcrux.rs +++ b/verdict/src/signature/ecdsa_libcrux.rs @@ -11,14 +11,14 @@ use verdict_parser::x509::*; verus! { -pub closed spec fn spec_p256_verify( +pub uninterp spec fn spec_p256_verify( alg: SpecAlgorithmIdentifierValue, pub_key: Seq, sig: Seq, msg: Seq, ) -> bool; -pub closed spec fn spec_p384_verify( +pub uninterp spec fn spec_p384_verify( alg: SpecAlgorithmIdentifierValue, pub_key: Seq, sig: Seq, diff --git a/verdict/src/signature/rsa_aws_lc.rs b/verdict/src/signature/rsa_aws_lc.rs index 8372ec6..b26311c 100644 --- a/verdict/src/signature/rsa_aws_lc.rs +++ b/verdict/src/signature/rsa_aws_lc.rs @@ -17,8 +17,8 @@ pub enum RSAError { pub struct RSAPublicKeyInternal(Vec); -pub closed spec fn spec_pkcs1_v1_5_load_pub_key(pub_key: Seq) -> Option; -pub closed spec fn spec_pkcs1_v1_5_verify( +pub uninterp spec fn spec_pkcs1_v1_5_load_pub_key(pub_key: Seq) -> Option; +pub uninterp spec fn spec_pkcs1_v1_5_verify( alg: SpecAlgorithmIdentifierValue, pub_key: RSAPublicKeyInternal, sig: Seq, @@ -44,7 +44,7 @@ pub closed spec fn spec_pkcs1_v1_5_verify( /// `msg` is the message expected to be signed #[verifier::external_body] pub fn pkcs1_v1_5_verify( - alg: &AlgorithmIdentifierValue, + alg: &AlgorithmIdentifierValue<'_>, pub_key: &RSAPublicKeyInternal, sig: &[u8], msg: &[u8], diff --git a/verdict/src/signature/rsa_libcrux.rs b/verdict/src/signature/rsa_libcrux.rs index c56142d..6dc9eea 100644 --- a/verdict/src/signature/rsa_libcrux.rs +++ b/verdict/src/signature/rsa_libcrux.rs @@ -30,8 +30,8 @@ pub struct RSAPublicKeyInternal { key: *mut u64, } -pub closed spec fn spec_pkcs1_v1_5_load_pub_key(pub_key: Seq) -> Option; -pub closed spec fn spec_pkcs1_v1_5_verify( +pub uninterp spec fn spec_pkcs1_v1_5_load_pub_key(pub_key: Seq) -> Option; +pub uninterp spec fn spec_pkcs1_v1_5_verify( alg: SpecAlgorithmIdentifierValue, pub_key: RSAPublicKeyInternal, sig: Seq, diff --git a/verdict/src/validator.rs b/verdict/src/validator.rs index ca9d9a3..eef7558 100644 --- a/verdict/src/validator.rs +++ b/verdict/src/validator.rs @@ -127,8 +127,7 @@ impl Query

{ pub open spec fn path_satisfies_policy(self, path: Seq, root_idx: usize) -> bool { let candidate = path.map_values(|i| self.bundle[i as int]) + seq![self.roots[root_idx as int]]; let abstract_candidate = candidate.map_values(|cert| policy::Certificate::spec_from(cert).unwrap()); - - self.policy.spec_valid_chain(abstract_candidate, self.task) matches Ok(res) && res + self.policy.spec_valid_chain(abstract_candidate, self.task) } pub open spec fn valid(self) -> bool { @@ -425,10 +424,7 @@ impl<'a, P: Policy> Validator<'a, P> { (path@.map_values(|i| cache.bundle@[i as int]) + seq![self.roots@[root_idx as int]]) .map_values(|cert| policy::Certificate::spec_from(cert).unwrap())); - match self.policy.valid_chain(&candidate, &cache.task) { - Ok(res) => Ok(res), - Err(err) => Err(ValidationError::PolicyError(err)), - } + Ok(self.policy.valid_chain(&candidate, &cache.task)) } /// Given a simple path through the bundle certificates @@ -465,7 +461,8 @@ impl<'a, P: Policy> Validator<'a, P> { forall |j| 0 <= j < i ==> !query.path_satisfies_policy(path@, #[trigger] root_issuers@[j]), { - #[cfg(trace)] eprintln_join!("checking path: ", format_dbg(path), " w/ root ", root_issuers[i]); + #[cfg(feature = "trace")] + eprintln_join!("checking path: ", format_dbg(path), " w/ root ", root_issuers[i]); if self.check_chain_policy(cache, &path, root_issuers[i])? { // Found a valid chain @@ -594,6 +591,7 @@ impl<'a, P: Policy> Validator<'a, P> { /// a task and try to build a valid chain through /// the `bundle` of intermediate certificates #[verifier::loop_isolation(false)] + #[verifier::exec_allows_no_decreases_clause] pub fn validate( &self, bundle: &VecDeep>,