verdict_parser/
lib.rs

1#![forbid(unsafe_code)]
2
3pub mod asn1;
4mod common;
5pub mod x509;
6
7pub use common::*;
8
9use vstd::prelude::*;
10
11verus! {
12    /// Top-level specification for x509 parsing from DER
13    pub closed spec fn spec_parse_x509_der(der: Seq<u8>) -> Option<x509::SpecCertificateValue> {
14        match x509::Certificate.spec_parse(der) {
15            Ok((n, cert)) if n == der.len() => Some(cert),
16            _ => None,
17        }
18    }
19
20    /// Spec for Base64 decoding
21    pub closed spec fn spec_decode_base64(base64: Seq<u8>) -> Option<Seq<u8>> {
22        match Base64.spec_parse(base64) {
23            Ok((n, bytes)) if n == base64.len() => Some(bytes),
24            _ => None,
25        }
26    }
27
28    /// Composition of `spec_parse_x509_der` and `spec_decode_base64`
29    pub open spec fn spec_parse_x509_base64(base64: Seq<u8>) -> Option<x509::SpecCertificateValue> {
30        match spec_decode_base64(base64) {
31            Some(der) => spec_parse_x509_der(der),
32            None => None,
33        }
34    }
35
36    /// Parses the given bytes in ASN.1 DER format
37    /// to a [`x509::CertificateValue`].
38    ///
39    /// This function has been formally verified for parsing soundness,
40    /// completeness, and non-malleability.
41    ///
42    /// NOTE: This is an internal function that is subject to change.
43    pub fn parse_x509_der<'a>(bytes: &'a [u8]) -> (res: Result<x509::CertificateValue<'a>, ParseError>)
44        ensures
45            res matches Ok(res) ==> {
46                // Soundness
47                &&& spec_parse_x509_der(bytes@) == Some(res@)
48
49                // Non-malleability
50                &&& forall |other: Seq<u8>| {
51                    &&& other.len() <= usize::MAX
52                    &&& #[trigger] spec_parse_x509_der(other) == Some(res@)
53                } ==> other == bytes@
54
55                // Prefix-security
56                &&& forall |suffix: Seq<u8>| {
57                    &&& suffix.len() != 0
58                    &&& bytes@.len() + suffix.len() <= usize::MAX
59                } ==> #[trigger] spec_parse_x509_der(bytes@ + suffix) is None
60            },
61
62            // Completeness
63            res is Err ==> spec_parse_x509_der(bytes@) is None,
64    {
65        let (n, cert) = x509::Certificate.parse(bytes)?;
66        if n != bytes.len() {
67            return Err(ParseError::Other("trailing bytes in certificate".to_string()));
68        }
69
70        proof {
71            let (n, spec_res) = x509::Certificate.spec_parse(bytes@).unwrap();
72
73            assert forall |other: Seq<u8>| {
74                &&& other.len() <= usize::MAX
75                &&& #[trigger] spec_parse_x509_der(other) == Some(cert@)
76            } implies other == bytes@ by {
77                let (m, other_res) = x509::Certificate.spec_parse(other).unwrap();
78                let other_ser = x509::Certificate.spec_serialize(other_res).unwrap();
79                let spec_ser = x509::Certificate.spec_serialize(spec_res).unwrap();
80
81                x509::Certificate.theorem_parse_serialize_roundtrip(other);
82                x509::Certificate.theorem_parse_serialize_roundtrip(bytes@);
83
84                assert(other_ser == other);
85                assert(other == spec_ser);
86                assert(spec_ser == bytes@);
87            }
88
89            assert forall |suffix: Seq<u8>|{
90                &&& suffix.len() != 0
91                &&& bytes@.len() + suffix.len() <= usize::MAX
92            } implies #[trigger] spec_parse_x509_der(bytes@ + suffix) is None by {
93                x509::Certificate.lemma_prefix_secure(bytes@, suffix);
94            }
95        }
96
97        Ok(cert)
98    }
99
100    /// Decodes a Base64-encoded sequence of bytes.
101    ///
102    /// This function has been formally verified for its
103    /// parsing soundness, completeness, and non-malleability.
104    ///
105    /// NOTE: This is an internal function that is subject to change.
106    pub fn decode_base64(encoded: &[u8]) -> (res: Result<Vec<u8>, ParseError>)
107        ensures
108            res matches Ok(res) ==> {
109                // Soundness
110                &&& spec_decode_base64(encoded@) == Some(res@)
111
112                // Non-malleability
113                &&& forall |other: Seq<u8>| {
114                    &&& other.len() <= usize::MAX
115                    &&& #[trigger] spec_decode_base64(other) == Some(res@)
116                } ==> other == encoded@
117            },
118
119            // Completeness
120            res is Err ==> spec_decode_base64(encoded@) is None,
121    {
122        let (n, bytes) = Base64.parse(encoded)?;
123
124        if n != encoded.len() {
125            return Err(ParseError::Other("trailing bytes in base64".to_string()));
126        }
127
128        assert(encoded.len() <= usize::MAX);
129        proof {
130            let (n, spec_res) = Base64.spec_parse(encoded@).unwrap();
131
132            assert forall |other: Seq<u8>| {
133                &&& other.len() <= usize::MAX
134                &&& #[trigger] spec_decode_base64(other) == Some(bytes@)
135            } implies other == encoded@ by {
136                let (_, other_res) = Base64.spec_parse(other).unwrap();
137                let other_ser = Base64.spec_serialize(other_res).unwrap();
138                let spec_ser = Base64.spec_serialize(spec_res).unwrap();
139
140                Base64.theorem_parse_serialize_roundtrip(other);
141                Base64.theorem_parse_serialize_roundtrip(encoded@);
142
143                assert(other_ser == other);
144                assert(other == spec_ser);
145                assert(spec_ser == encoded@);
146            }
147        }
148
149        Ok(bytes)
150    }
151}
verdict_parser/lib.rs

verdict_parser/
lib.rs
