verdict_parser/x509/
cert.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6// Certificate  ::=  SEQUENCE  {
7//     tbsCertificate       TBSCertificate,
8//     signatureAlgorithm   AlgorithmIdentifier,
9//     signatureValue       BIT STRING
10// }
11asn1! {
12    seq CertificateInner {
13        cert: Cached<ASN1<TBSCertificate>> = Cached(ASN1(TBSCertificate)),
14        sig_alg: Cached<ASN1<AlgorithmIdentifier>> = Cached(ASN1(AlgorithmIdentifier)),
15        sig: ASN1<BitString> = ASN1(BitString),
16    }
17}
18
19wrap_combinator! {
20    pub struct Certificate: Cached<ASN1<CertificateInner>> = Cached(ASN1(CertificateInner));
21}
22
23pub type SpecCertificateValue = SpecCertificateInnerValue;
24pub type CertificateValue<'a> = CachedValue<'a, ASN1<CertificateInner>>;
25
26}
27
28#[cfg(test)]
29mod test {
30    #![allow(unused_variables)]
31
32    use super::*;
33    use base64::Engine;
34
35    verus! {
36        /// Check that all trait bounds and preconditions are satisfied
37        #[test]
38        fn is_combinator() {
39            let _ = Certificate.parse(&[]);
40        }
41
42        /// Check if the serialization cache is correct
43        #[test]
44        fn cached() {
45            if let Ok((_, res)) = Certificate.parse(&[]) {
46                let ser = res.serialize();
47                assert(ASN1(CertificateInner)@.spec_serialize(res@).is_ok());
48                assert(ser@ == ASN1(CertificateInner)@.spec_serialize(res@).unwrap());
49
50                let tbs: &CachedValue<ASN1<TBSCertificate>> = &res.get().cert;
51                let tbs_ser = tbs.serialize();
52                assert(ASN1(TBSCertificate)@.spec_serialize(tbs@).is_ok());
53                assert(tbs_ser@ == ASN1(TBSCertificate)@.spec_serialize(tbs@).unwrap());
54            }
55        }
56    }
57
58    fn parse_cert(src: &str) -> Result<(), String> {
59        let cert_base64 = src.split_whitespace().collect::<String>();
60        let cert_bytes = base64::prelude::BASE64_STANDARD
61            .decode(cert_base64)
62            .map_err(|e| format!("Failed to decode Base64: {}", e))?;
63
64        let (n, cert) = Certificate
65            .parse(&cert_bytes)
66            .map_err(|e| format!("Failed to parse certificate"))?;
67
68        // Check that the caching is correct
69        assert_eq!(n, cert_bytes.len());
70        assert_eq!(&cert_bytes, cert.serialize());
71
72        Ok(())
73    }
74
75    /// Test the final combinator on some root certificates
76    #[test]
77    fn roots_pem() {
78        let roots = include_str!("../../tests/data/roots.pem");
79        const PREFIX: &'static str = "-----BEGIN CERTIFICATE-----";
80        const SUFFIX: &'static str = "-----END CERTIFICATE-----";
81
82        // Parse all certificates provided
83        roots
84            .split(PREFIX)
85            .skip(1)
86            .enumerate()
87            .for_each(|(i, cert_enc)| match cert_enc.split(SUFFIX).next() {
88                Some(cert_enc) => {
89                    eprintln!("Parsing certificate {}", i);
90                    assert!(parse_cert(cert_enc).is_ok());
91                }
92                None => {}
93            });
94    }
95}
verdict_parser/x509/cert.rs

verdict_parser/x509/
cert.rs
