verdict_parser/asn1/
oid.rs

1use super::*;
2use std::fmt::{self, Debug, Formatter};
3use vstd::prelude::*;
4
5verus! {
6
7/// Combinator for ASN.1 Object Identifier
8#[derive(Debug, View)]
9pub struct ObjectIdentifier;
10
11asn1_tagged!(ObjectIdentifier, tag_of!(OBJECT_IDENTIFIER));
12
13pub type SpecObjectIdentifierValue = Seq<UInt>;
14#[derive(PolyfillClone, Eq, PartialEq)]
15pub struct ObjectIdentifierValue(pub VecDeep<UInt>);
16pub type ObjectIdentifierValueOwned = ObjectIdentifierValue;
17
18impl View for ObjectIdentifierValue {
19    type V = Seq<UInt>;
20
21    open spec fn view(&self) -> Self::V {
22        self.0@
23    }
24}
25
26impl PolyfillEq for ObjectIdentifierValue {
27    #[inline(always)]
28    fn polyfill_eq(&self, other: &ObjectIdentifierValue) -> bool
29    {
30        self.0.polyfill_eq(&other.0)
31    }
32}
33
34impl ObjectIdentifier {
35    /// First byte of an OID is 40 * arc1 + arc2
36    closed spec fn parse_first_two_arcs(byte: u8) -> Option<(UInt, UInt)> {
37        let arc1 = byte / 40;
38        let arc2 = byte % 40;
39
40        if arc1 <= 2 && arc2 <= 39 {
41            Some((arc1 as UInt, arc2 as UInt))
42        } else {
43            None
44        }
45    }
46
47    closed spec fn serialize_first_two_arcs(arc1: UInt, arc2: UInt) -> Option<u8> {
48        if arc1 <= 2 && arc2 <= 39 {
49            Some((arc1 * 40 + arc2) as u8)
50        } else {
51            None
52        }
53    }
54
55    proof fn lemma_serialize_parse_first_two_arcs(arc1: UInt, arc2: UInt)
56        ensures
57            Self::serialize_first_two_arcs(arc1, arc2) matches Some(byte) ==>
58                Self::parse_first_two_arcs(byte) == Some((arc1, arc2))
59    {}
60
61    proof fn lemma_parse_serialize_first_two_arcs(byte: u8)
62        ensures
63            Self::parse_first_two_arcs(byte) matches Some((arc1, arc2)) ==>
64                Self::serialize_first_two_arcs(arc1, arc2) == Some(byte)
65    {}
66}
67
68impl SpecCombinator for ObjectIdentifier {
69    type SpecResult = SpecObjectIdentifierValue;
70
71    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
72        match new_spec_object_identifier_inner().spec_parse(s) {
73            Ok((len, (_, (first, rest_arcs)))) =>
74                match Self::parse_first_two_arcs(first) {
75                    Some((arc1, arc2)) =>
76                        if rest_arcs.len() + 2 <= usize::MAX {
77                            Ok((len, seq![ arc1, arc2 ] + rest_arcs))
78                        } else {
79                            Err(())
80                        }
81                    None => Err(()),
82                }
83
84            Err(..) => Err(()),
85        }
86    }
87
88    proof fn spec_parse_wf(&self, s: Seq<u8>) {
89        new_spec_object_identifier_inner().spec_parse_wf(s);
90    }
91
92    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
93        if v.len() < 2 || v.len() > usize::MAX {
94            Err(())
95        } else {
96            match Self::serialize_first_two_arcs(v[0], v[1]) {
97                Some(first_byte) => {
98                    let rest_arcs = v.skip(2);
99
100                    // Compute the inner length first
101                    // TODO: how to avoid this?
102                    match (U8, Repeat(Base128UInt)).spec_serialize((first_byte, rest_arcs)) {
103                        Ok(buf) =>
104                            new_spec_object_identifier_inner().spec_serialize((buf.len() as LengthValue, (first_byte, rest_arcs))),
105                        Err(..) => Err(())
106                    }
107                },
108                None => Err(()),
109            }
110        }
111    }
112}
113
114impl SecureSpecCombinator for ObjectIdentifier {
115    open spec fn is_prefix_secure() -> bool {
116        true
117    }
118
119    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
120        if let Ok(b) = self.spec_serialize(v) {
121            let first_byte = Self::serialize_first_two_arcs(v[0], v[1]).unwrap();
122            let rest_arcs = v.skip(2);
123            let buf = (U8, Repeat(Base128UInt)).spec_serialize((first_byte, rest_arcs)).unwrap();
124
125            new_spec_object_identifier_inner().theorem_serialize_parse_roundtrip((buf.len() as LengthValue, (first_byte, rest_arcs)));
126            Self::lemma_serialize_parse_first_two_arcs(v[0], v[1]);
127
128            let (len, v2) = self.spec_parse(b).unwrap();
129            assert(len == b.len() as usize);
130            assert(v2 =~= v);
131        }
132    }
133
134    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
135        if let Ok((len, v)) = self.spec_parse(buf) {
136            let (_, (_, (first_byte, rest_arcs))) = new_spec_object_identifier_inner().spec_parse(buf).unwrap();
137
138            new_spec_object_identifier_inner().theorem_parse_serialize_roundtrip(buf);
139            Self::lemma_parse_serialize_first_two_arcs(first_byte);
140
141            assert(v.skip(2) =~= rest_arcs);
142
143            let buf2 = self.spec_serialize(v).unwrap();
144            assert(buf2 =~= buf.subrange(0, len as int));
145        }
146    }
147
148    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
149        new_spec_object_identifier_inner().lemma_prefix_secure(s1, s2);
150    }
151}
152
153impl Combinator for ObjectIdentifier {
154    type Result<'a> = ObjectIdentifierValue;
155    type Owned = ObjectIdentifierValueOwned;
156
157    closed spec fn spec_length(&self) -> Option<usize> {
158        None
159    }
160
161    fn length(&self) -> Option<usize> {
162        None
163    }
164
165    #[inline]
166    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
167        let (len, (_, (first, mut rest_arcs))) = new_object_identifier_inner().parse(s)?;
168
169        let arc1 = first / 40;
170        let arc2 = first % 40;
171
172        if arc1 > 2 || arc2 > 39 {
173            return Err(ParseError::Other("Invalid first two arcs".to_string()));
174        }
175
176        if rest_arcs.len() > usize::MAX - 2 {
177            return Err(ParseError::SizeOverflow);
178        }
179
180        let mut res = VecDeep::with_capacity(2 + rest_arcs.len());
181        res.push(arc1 as UInt);
182        res.push(arc2 as UInt);
183        res.append(&mut rest_arcs);
184
185        assert(res@ == self.spec_parse(s@).unwrap().1);
186
187        Ok((len, ObjectIdentifierValue(res)))
188    }
189
190    #[inline]
191    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
192        let mut v = v.0;
193        let ghost old_v = v@;
194
195        if v.len() < 2 {
196            return Err(SerializeError::Other("OID should have at least two arcs".to_string()));
197        }
198
199        if *v.get(0) > 2 || *v.get(1) > 39 {
200            return Err(SerializeError::Other("Invalid first two arcs".to_string()));
201        }
202
203        let first_byte = *v.get(0) as u8 * 40 + *v.get(1) as u8;
204
205        let rest_arcs_inner = v.split_off(2);
206
207        // Need to figure out the content length first
208        // TODO: this seems inefficient
209        let rest_arcs_cloned = PolyfillClone::clone(&rest_arcs_inner);
210        let rest_arcs = rest_arcs_inner;
211
212        let len = (U8, Repeat(Base128UInt)).serialize((first_byte, rest_arcs_cloned), data, pos)?;
213        let len2 = new_object_identifier_inner().serialize((len as LengthValue, (first_byte, rest_arcs)), data, pos)?;
214
215        if pos.checked_add(len2).is_some() && pos + len2 <= data.len() {
216            assert(rest_arcs_cloned@ == old_v.skip(2));
217            assert(data@ =~= seq_splice(old(data)@, pos, self.spec_serialize(old_v).unwrap()));
218
219            return Ok(len2);
220        }
221
222        Err(SerializeError::InsufficientBuffer)
223    }
224}
225
226/// The function |i| AndThen(Bytes(i as usize), (U8, Repeat(Base128UInt)))
227struct OIDCont;
228
229impl Continuation for OIDCont {
230    type Input<'a> = LengthValue;
231    type Output = AndThen<Bytes, (U8, Repeat<Base128UInt>)>;
232
233    #[inline(always)]
234    fn apply<'a>(&self, i: Self::Input<'a>) -> (o: Self::Output) {
235        AndThen(Bytes(i as usize), (U8, Repeat(Base128UInt)))
236    }
237
238    closed spec fn requires<'a>(&self, i: Self::Input<'a>) -> bool {
239        true
240    }
241
242    closed spec fn ensures<'a>(&self, i: Self::Input<'a>, o: Self::Output) -> bool {
243        o == AndThen(Bytes(i as usize), (U8, Repeat(Base128UInt)))
244    }
245}
246
247/// The inner version parses a length first
248/// then read a single byte (for the first two arcs)
249/// and then repeatedly read a sequence of Base128UInt's
250#[allow(dead_code)]
251type SpecObjectIdentifierInner = SpecDepend<Length, AndThen<Bytes, (U8, Repeat<Base128UInt>)>>;
252type ObjectIdentifierInner = Depend<Length, AndThen<Bytes, (U8, Repeat<Base128UInt>)>, OIDCont>;
253
254closed spec fn new_spec_object_identifier_inner() -> SpecObjectIdentifierInner {
255    SpecDepend {
256        fst: Length,
257        snd: |l| {
258            AndThen(Bytes(l as usize), (U8, Repeat(Base128UInt)))
259        },
260    }
261}
262
263#[inline(always)]
264fn new_object_identifier_inner() -> (res: ObjectIdentifierInner)
265    ensures res@ == new_spec_object_identifier_inner()
266{
267    Depend {
268        fst: Length,
269        snd: OIDCont,
270        spec_snd: Ghost(|l| {
271            AndThen(Bytes(l as usize), (U8, Repeat(Base128UInt)))
272        }),
273    }
274}
275
276}
277
278impl Debug for ObjectIdentifierValue {
279    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
280        write!(f, "OID(")?;
281
282        for (i, arc) in self.0 .0.iter().enumerate() {
283            if i != 0 {
284                write!(f, ".")?;
285            }
286
287            write!(f, "{}", arc)?;
288        }
289
290        write!(f, ")")
291    }
292}
293
294#[cfg(test)]
295mod tests {
296    use super::*;
297    use der::Encode;
298
299    fn serialize_oid(v: Vec<UInt>) -> Result<Vec<u8>, SerializeError> {
300        let mut data = vec![0; 1 + 4 + v.len() * 8];
301        data[0] = 0x06;
302        let len = ObjectIdentifier.serialize(
303            ObjectIdentifierValue(VecDeep::from_vec(v)),
304            &mut data,
305            1,
306        )?;
307        data.truncate(len + 1);
308        Ok(data)
309    }
310
311    #[test]
312    fn diff_with_der() {
313        let diff = |v: Vec<UInt>| {
314            let res1 = serialize_oid(PolyfillClone::clone(&v)).map_err(|_| ());
315            let res2 = der::asn1::ObjectIdentifier::new_unwrap(
316                v.iter()
317                    .map(|i| i.to_string())
318                    .collect::<Vec<_>>()
319                    .join(".")
320                    .as_str(),
321            )
322            .to_der()
323            .map_err(|_| ());
324
325            assert_eq!(res1, res2);
326        };
327
328        diff(vec![1, 2, 3]);
329        diff(vec![1, 2, 123214]);
330        diff(vec![1, 2, 123214, 1231, 4534, 231]);
331        diff(vec![2, 10, 123214, 1231, 4534, 231]);
332        diff(vec![2, 39, 123214, 1231, 4534, 231]);
333    }
334}
verdict_parser/asn1/oid.rs

verdict_parser/asn1/
oid.rs
