verdict_parser/asn1/
tag.rs

1use super::*;
2use vstd::prelude::*;
3use vstd::slice::slice_subrange;
4
5verus! {
6
7/// Combinator for ASN.1 tags
8#[derive(Debug, View)]
9pub struct ASN1Tag;
10
11#[derive(Debug)]
12pub struct TagValue {
13    pub class: TagClass,
14    pub form: TagForm,
15
16    /// Currently we only support tag numbers up to 31
17    /// Larger tag numbers require the long form of tags
18    pub num: u8,
19}
20
21impl View for TagValue {
22    type V = TagValue;
23
24    open spec fn view(&self) -> Self::V {
25        *self
26    }
27}
28
29#[derive(Debug)]
30pub enum TagClass {
31    Universal,
32    Application,
33    ContextSpecific,
34    Private,
35}
36
37#[derive(Debug)]
38pub enum TagForm {
39    Primitive,
40    Constructed,
41}
42
43impl TagValue {
44    #[inline(always)]
45    pub fn eq(self, other: TagValue) -> (res: bool)
46        ensures res == (self == other)
47    {
48        // TODO: fix this once Verus supports equality for enum
49        (match (self.class, other.class) {
50            (TagClass::Universal, TagClass::Universal) => true,
51            (TagClass::Application, TagClass::Application) => true,
52            (TagClass::ContextSpecific, TagClass::ContextSpecific) => true,
53            (TagClass::Private, TagClass::Private) => true,
54            _ => false,
55        }) && (match (self.form, other.form) {
56            (TagForm::Primitive, TagForm::Primitive) => true,
57            (TagForm::Constructed, TagForm::Constructed) => true,
58            _ => false,
59        }) && self.num == other.num
60    }
61
62    /// TODO: fix after Verus supports Clone
63    #[inline(always)]
64    pub fn clone(&self) -> (res: TagValue)
65        ensures res == *self
66    {
67        TagValue {
68            class: match self.class {
69                TagClass::Universal => TagClass::Universal,
70                TagClass::Application => TagClass::Application,
71                TagClass::ContextSpecific => TagClass::ContextSpecific,
72                TagClass::Private => TagClass::Private,
73            },
74            form: match self.form {
75                TagForm::Primitive => TagForm::Primitive,
76                TagForm::Constructed => TagForm::Constructed,
77            },
78            num: self.num,
79        }
80    }
81}
82
83impl SpecCombinator for ASN1Tag {
84    type SpecResult = TagValue;
85
86    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
87        if s.len() == 0 {
88            Err(())
89        } else {
90            let class_num = s[0] >> 6 & 0b11;
91            let class = if class_num == 0 {
92                TagClass::Universal
93            } else if class_num == 1 {
94                TagClass::Application
95            } else if class_num == 2 {
96                TagClass::ContextSpecific
97            } else {
98                TagClass::Private
99            };
100
101            let form_num = s[0] >> 5 & 1;
102            let form = if form_num == 0 {
103                TagForm::Primitive
104            } else {
105                TagForm::Constructed
106            };
107
108            Ok((1, TagValue {
109                class,
110                form,
111                num: s[0] & 0b11111,
112            }))
113        }
114    }
115
116    proof fn spec_parse_wf(&self, s: Seq<u8>) {}
117
118    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
119        let class: u8 = match v.class {
120            TagClass::Universal => 0,
121            TagClass::Application => 1,
122            TagClass::ContextSpecific => 2,
123            _ => 3,
124        };
125
126        let form: u8 = match v.form {
127            TagForm::Primitive => 0,
128            _ => 1,
129        };
130
131        if v.num > 0b11111 {
132            Err(())
133        } else {
134            Ok(seq![(class << 6) | (form << 5) | (v.num & 0b11111)])
135        }
136    }
137}
138
139impl SecureSpecCombinator for ASN1Tag {
140    open spec fn is_prefix_secure() -> bool {
141        true
142    }
143
144    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
145        let class_num: u8 = match v.class {
146            TagClass::Universal => 0,
147            TagClass::Application => 1,
148            TagClass::ContextSpecific => 2,
149            _ => 3,
150        };
151
152        let form_num: u8 = match v.form {
153            TagForm::Primitive => 0,
154            _ => 1,
155        };
156
157        let num = v.num;
158
159        // Restate parse(serialize(v)) = v, but purely in BV
160        assert(
161            0 <= class_num < 4 &&
162            0 <= form_num < 2 &&
163            0 <= num <= 0b11111 ==> {
164            let ser = (class_num << 6) | (form_num << 5) | (num & 0b11111);
165            &&& ser >> 6 & 0b11 == class_num
166            &&& ser >> 5 & 1 == form_num
167            &&& ser & 0b11111 == num
168        }) by (bit_vector);
169    }
170
171    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
172        let tag = buf[0];
173
174        // Restate serialize(parse(v)) = v, but purely in BV
175        assert(
176            (tag >> 6 & 0b11) << 6 | (tag >> 5 & 1) << 5 | ((tag & 0b11111) & 0b11111) == tag
177        ) by (bit_vector);
178
179        // Some bound facts
180        assert(tag >> 6 & 0b11 < 4) by (bit_vector);
181        assert(tag >> 5 & 1 < 2) by (bit_vector);
182        assert(tag & 0b11111 <= 0b11111) by (bit_vector);
183
184        if let Ok((n, v)) = self.spec_parse(buf) {
185            let ser = self.spec_serialize(v).unwrap();
186            assert(ser =~= buf.subrange(0, 1));
187        }
188    }
189
190    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {}
191}
192
193impl Combinator for ASN1Tag {
194    type Result<'a> = TagValue;
195    type Owned = TagValue;
196
197    closed spec fn spec_length(&self) -> Option<usize> {
198        Some(1)
199    }
200
201    fn length(&self) -> Option<usize> {
202        Some(1)
203    }
204
205    #[inline]
206    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
207        if s.len() == 0 {
208            return Err(ParseError::UnexpectedEndOfInput);
209        } else {
210            let class_num = s[0] >> 6 & 0b11;
211            let class = if class_num == 0 {
212                TagClass::Universal
213            } else if class_num == 1 {
214                TagClass::Application
215            } else if class_num == 2 {
216                TagClass::ContextSpecific
217            } else {
218                TagClass::Private
219            };
220
221            let form_num = s[0] >> 5 & 1;
222            let form = if form_num == 0 {
223                TagForm::Primitive
224            } else {
225                TagForm::Constructed
226            };
227
228            Ok((1, TagValue {
229                class,
230                form,
231                num: s[0] & 0b11111,
232            }))
233        }
234    }
235
236    #[inline]
237    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
238        let class: u8 = match v.class {
239            TagClass::Universal => 0,
240            TagClass::Application => 1,
241            TagClass::ContextSpecific => 2,
242            _ => 3,
243        };
244
245        let form: u8 = match v.form {
246            TagForm::Primitive => 0,
247            _ => 1,
248        };
249
250        if v.num > 0b11111 {
251            return Err(SerializeError::Other("Invalid tag number".to_string()));
252        }
253
254        if pos < data.len() {
255            let tag = (class << 6) | (form << 5) | (v.num & 0b11111);
256            data.set(pos, tag);
257            assert(data@ == seq_splice(old(data)@, pos, seq![tag]));
258            Ok(1)
259        } else {
260            Err(SerializeError::InsufficientBuffer)
261        }
262    }
263}
264
265/// A trait for combinators to mark their original tags
266/// (e.g. 0x02 for INTEGER)
267///
268/// Can be overwritten by explicit or implicit tagging
269pub trait ASN1Tagged
270{
271    spec fn spec_tag(&self) -> TagValue;
272    fn tag(&self) -> (res: TagValue)
273        ensures res == self.spec_tag();
274}
275
276/// An additional property that if an ASN1Tagged
277/// implements View, then the viewed version preserves the tag
278pub trait ViewWithASN1Tagged: View + ASN1Tagged where
279    Self::V: ASN1Tagged,
280{
281    proof fn lemma_view_preserves_tag(&self)
282        ensures self@.spec_tag() == self.spec_tag();
283}
284
285/// A combinator wrapper that also emits a tag before
286/// parsing/serializing the inner value
287#[derive(Debug)]
288pub struct ASN1<T>(pub T);
289
290impl<T: View> View for ASN1<T> {
291    type V = ASN1<T::V>;
292
293    open spec fn view(&self) -> Self::V {
294        ASN1(self.0.view())
295    }
296}
297
298impl<T: ASN1Tagged> ASN1Tagged for ASN1<T> {
299    open spec fn spec_tag(&self) -> TagValue {
300        self.0.spec_tag()
301    }
302
303    #[inline(always)]
304    fn tag(&self) -> TagValue {
305        self.0.tag()
306    }
307}
308
309impl<T: ASN1Tagged + ViewWithASN1Tagged> ViewWithASN1Tagged for ASN1<T> where
310    T::V: ASN1Tagged,
311{
312    proof fn lemma_view_preserves_tag(&self) {
313        self.0.lemma_view_preserves_tag();
314    }
315}
316
317impl<T: ASN1Tagged + SpecCombinator> SpecCombinator for ASN1<T> {
318    type SpecResult = <T as SpecCombinator>::SpecResult;
319
320    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
321        match (ASN1Tag, self.0).spec_parse(s) {
322            Ok((n, (tag, v))) =>
323                if tag == self.0.spec_tag() {
324                    Ok((n, v))
325                } else {
326                    Err(())
327                }
328            Err(()) => Err(()),
329        }
330    }
331
332    proof fn spec_parse_wf(&self, s: Seq<u8>) {
333        (ASN1Tag, self.0).spec_parse_wf(s);
334    }
335
336    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
337        (ASN1Tag, self.0).spec_serialize((self.0.spec_tag(), v))
338    }
339}
340
341impl<T: ASN1Tagged + SecureSpecCombinator> SecureSpecCombinator for ASN1<T> {
342    open spec fn is_prefix_secure() -> bool {
343        T::is_prefix_secure()
344    }
345
346    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
347        (ASN1Tag, self.0).theorem_serialize_parse_roundtrip((self.0.spec_tag(), v));
348    }
349
350    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
351        (ASN1Tag, self.0).theorem_parse_serialize_roundtrip(buf);
352    }
353
354    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
355        (ASN1Tag, self.0).lemma_prefix_secure(s1, s2);
356    }
357}
358
359impl<T: ASN1Tagged + Combinator> Combinator for ASN1<T> where
360    // T: SecureSpecCombinator<SpecResult = <<T as Combinator>::Owned as View>::V>,
361    <T as View>::V: SecureSpecCombinator<SpecResult = <<T as Combinator>::Owned as View>::V>,
362    <T as View>::V: ASN1Tagged,
363    T: ViewWithASN1Tagged,
364{
365    type Result<'a> = T::Result<'a>;
366    type Owned = T::Owned;
367
368    open spec fn spec_length(&self) -> Option<usize> {
369        match self.0.spec_length() {
370            Some(len) => len.checked_add(1),
371            None => None,
372        }
373    }
374
375    fn length(&self) -> Option<usize> {
376        match self.0.length() {
377            Some(len) => len.checked_add(1),
378            None => None,
379        }
380    }
381
382    open spec fn parse_requires(&self) -> bool {
383        self.0.parse_requires()
384    }
385
386    #[inline(always)]
387    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
388        proof {
389            self.0.lemma_view_preserves_tag();
390        }
391
392        let (n1, tag) = ASN1Tag.parse(s)?;
393        let (n2, v) = self.0.parse(slice_subrange(s, n1, s.len()))?;
394
395        if tag.eq(self.0.tag()) && n1 <= usize::MAX - n2 {
396            Ok((n1 + n2, v))
397        } else {
398            Err(ParseError::Other("Unmatching tags".to_string()))
399        }
400    }
401
402    open spec fn serialize_requires(&self) -> bool {
403        self.0.serialize_requires()
404    }
405
406    #[inline(always)]
407    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
408        proof {
409            self.0.lemma_view_preserves_tag();
410        }
411
412        let n1 = ASN1Tag.serialize(self.0.tag(), data, pos)?;
413        if n1 > usize::MAX - pos || n1 + pos > data.len() {
414            return Err(SerializeError::InsufficientBuffer);
415        }
416
417        let n2 = self.0.serialize(v, data, pos + n1)?;
418
419        if n1 <= usize::MAX - n2 {
420            assert(data@ =~= seq_splice(old(data)@, pos, self@.spec_serialize(v@).unwrap()));
421            Ok(n1 + n2)
422        } else {
423            Err(SerializeError::SizeOverflow)
424        }
425    }
426}
427
428/// If T1 and T2 have different tags, then their tagged encodings are disjoint
429impl<T1, T2> DisjointFrom<ASN1<T1>> for ASN1<T2> where
430    T1: ASN1Tagged + SpecCombinator,
431    T2: ASN1Tagged + SpecCombinator,
432{
433    open spec fn disjoint_from(&self, other: &ASN1<T1>) -> bool {
434        self.0.spec_tag() != other.0.spec_tag()
435    }
436
437    proof fn parse_disjoint_on(&self, other: &ASN1<T1>, buf: Seq<u8>) {}
438}
439
440/// If T1 and T2 have different tags, then (T1, ...) is disjoint from T2
441impl<T1, T2, S> DisjointFrom<(ASN1<T1>, S)> for ASN1<T2> where
442    T1: ASN1Tagged + SpecCombinator + SecureSpecCombinator,
443    T2: ASN1Tagged + SpecCombinator,
444    S: SpecCombinator,
445{
446    open spec fn disjoint_from(&self, other: &(ASN1<T1>, S)) -> bool {
447        self.0.spec_tag() != other.0.0.spec_tag()
448    }
449
450    proof fn parse_disjoint_on(&self, other: &(ASN1<T1>, S), buf: Seq<u8>) {}
451}
452
453// NOTE: We can't do impl<T1, T2, S> SpecDisjointFrom<ASN1<T2>> for (ASN1<T1>, S) since
454// both SpecDisjointFrom and tuple type is not defined in this crate
455// For this purpose, use Pair instead of the native tuple type
456
457/// Same as above, but uses a custom
458impl<T1, T2, S> DisjointFrom<Pair<ASN1<T1>, S>> for ASN1<T2> where
459    T1: ASN1Tagged + SecureSpecCombinator,
460    T2: ASN1Tagged + SecureSpecCombinator,
461    S: SecureSpecCombinator,
462{
463    open spec fn disjoint_from(&self, other: &Pair<ASN1<T1>, S>) -> bool {
464        self.0.spec_tag() != other.0.0.spec_tag()
465    }
466
467    proof fn parse_disjoint_on(&self, other: &Pair<ASN1<T1>, S>, buf: Seq<u8>) {}
468}
469
470/// The other direction of the above
471impl<T1, T2, S> DisjointFrom<ASN1<T2>> for Pair<ASN1<T1>, S> where
472    T1: ASN1Tagged + SecureSpecCombinator,
473    T2: ASN1Tagged + SecureSpecCombinator,
474    S: SecureSpecCombinator,
475{
476    open spec fn disjoint_from(&self, other: &ASN1<T2>) -> bool {
477        other.0.spec_tag() != self.0.0.spec_tag()
478    }
479
480    proof fn parse_disjoint_on(&self, other: &ASN1<T2>, buf: Seq<u8>) {}
481}
482
483impl<T> DisjointFrom<ASN1<T>> for End where
484    T: ASN1Tagged + SpecCombinator,
485{
486    open spec fn disjoint_from(&self, other: &ASN1<T>) -> bool { true }
487    proof fn parse_disjoint_on(&self, other: &ASN1<T>, buf: Seq<u8>) {}
488}
489
490impl<T1, T2> DisjointFrom<ASN1<T1>> for Cond<ASN1<T2>> where
491    T1: ASN1Tagged + SpecCombinator,
492    T2: ASN1Tagged + SpecCombinator,
493 {
494    open spec fn disjoint_from(&self, other: &ASN1<T1>) -> bool {
495        self.inner.0.spec_tag() != other.0.spec_tag()
496    }
497
498    proof fn parse_disjoint_on(&self, other: &ASN1<T1>, buf: Seq<u8>) {}
499}
500
501impl<T1, T2> DisjointFrom<Cached<ASN1<T1>>> for ASN1<T2> where
502    T1: ASN1Tagged + SpecCombinator,
503    T2: ASN1Tagged + SpecCombinator,
504{
505    open spec fn disjoint_from(&self, other: &Cached<ASN1<T1>>) -> bool {
506        self.0.spec_tag() != other.0.0.spec_tag()
507    }
508
509    proof fn parse_disjoint_on(&self, other: &Cached<ASN1<T1>>, buf: Seq<u8>) {}
510}
511
512impl<T1, T2, S> DisjointFrom<Cached<ASN1<T2>>> for Pair<ASN1<T1>, S> where
513    T1: ASN1Tagged + SecureSpecCombinator,
514    T2: ASN1Tagged + SecureSpecCombinator,
515    S: SecureSpecCombinator,
516{
517    open spec fn disjoint_from(&self, other: &Cached<ASN1<T2>>) -> bool {
518        other.0.0.spec_tag() != self.0.0.spec_tag()
519    }
520
521    proof fn parse_disjoint_on(&self, other: &Cached<ASN1<T2>>, buf: Seq<u8>) {}
522}
523
524/// Macro to generate a ASN1Tagged and ViewWithASN1Tagged trait impl
525#[allow(unused_macros)]
526#[macro_export]
527macro_rules! asn1_tagged {
528    ($ty:ident, $tag:expr) => {
529        ::builtin_macros::verus! {
530            impl ASN1Tagged for $ty {
531                open spec fn spec_tag(&self) -> TagValue {
532                    $tag
533                }
534
535                fn tag(&self) -> TagValue {
536                    $tag
537                }
538            }
539
540            impl ViewWithASN1Tagged for $ty {
541                proof fn lemma_view_preserves_tag(&self) {}
542            }
543        }
544    };
545}
546pub use asn1_tagged;
547
548/// Tags of common ASN.1 types
549#[allow(unused_macros)]
550macro_rules! tag_of {
551    (BOOLEAN) => {
552        TagValue {
553            class: TagClass::Universal,
554            form: TagForm::Primitive,
555            num: 0x01,
556        }
557    };
558
559    (INTEGER) => {
560        TagValue {
561            class: TagClass::Universal,
562            form: TagForm::Primitive,
563            num: 0x02,
564        }
565    };
566
567    (BIT_STRING) => {
568        TagValue {
569            class: TagClass::Universal,
570            form: TagForm::Primitive,
571            num: 0x03,
572        }
573    };
574
575    (OCTET_STRING) => {
576        TagValue {
577            class: TagClass::Universal,
578            form: TagForm::Primitive,
579            num: 0x04,
580        }
581    };
582
583    (NULL) => {
584        TagValue {
585            class: TagClass::Universal,
586            form: TagForm::Primitive,
587            num: 0x05,
588        }
589    };
590
591    (OBJECT_IDENTIFIER) => {
592        TagValue {
593            class: TagClass::Universal,
594            form: TagForm::Primitive,
595            num: 0x06,
596        }
597    };
598
599    (SEQUENCE) => {
600        TagValue {
601            class: TagClass::Universal,
602            form: TagForm::Constructed,
603            num: 0x10,
604        }
605    };
606
607    (SET) => {
608        TagValue {
609            class: TagClass::Universal,
610            form: TagForm::Constructed,
611            num: 0x11,
612        }
613    };
614
615    (UTF8_STRING) => {
616        TagValue {
617            class: TagClass::Universal,
618            form: TagForm::Primitive,
619            num: 0x0c,
620        }
621    };
622
623    (PRINTABLE_STRING) => {
624        TagValue {
625            class: TagClass::Universal,
626            form: TagForm::Primitive,
627            num: 0x13,
628        }
629    };
630
631    (TELETEX_STRING) => {
632        TagValue {
633            class: TagClass::Universal,
634            form: TagForm::Primitive,
635            num: 0x14,
636        }
637    };
638
639    (IA5_STRING) => {
640        TagValue {
641            class: TagClass::Universal,
642            form: TagForm::Primitive,
643            num: 0x16,
644        }
645    };
646
647    (UNIVERSAL_STRING) => {
648        TagValue {
649            class: TagClass::Universal,
650            form: TagForm::Primitive,
651            num: 0x1c,
652        }
653    };
654
655    (BMP_STRING) => {
656        TagValue {
657            class: TagClass::Universal,
658            form: TagForm::Primitive,
659            num: 0x1e,
660        }
661    };
662
663    (UTC_TIME) => {
664        TagValue {
665            class: TagClass::Universal,
666            form: TagForm::Primitive,
667            num: 0x17,
668        }
669    };
670
671    (GENERALIZED_TIME) => {
672        TagValue {
673            class: TagClass::Universal,
674            form: TagForm::Primitive,
675            num: 0x18,
676        }
677    };
678
679    (IMPLICIT $num:literal) => {
680        TagValue {
681            class: TagClass::ContextSpecific,
682            form: TagForm::Primitive,
683            num: $num,
684        }
685    };
686
687    (EXPLICIT $num:literal) => {
688        TagValue {
689            class: TagClass::ContextSpecific,
690            form: TagForm::Constructed,
691            num: $num,
692        }
693    };
694}
695pub(crate) use tag_of;
696
697/// Placeholder to parse a TLV tuple as OctetString
698/// with the provided tag
699#[allow(unused_macros)]
700macro_rules! placeholder {
701    ($($tag:tt)*) => {
702        ASN1(ImplicitTag(tag_of!($($tag)*), OctetString))
703    };
704}
705pub(crate) use placeholder;
706
707#[allow(unused_macros)]
708macro_rules! placeholder_type {
709    () => { ASN1<ImplicitTag<OctetString>> };
710}
711pub(crate) use placeholder_type;
712
713// #[allow(unused_macros)]
714// macro_rules! implicit_tag {
715//     ($num:literal, $inner:expr) => {
716//         ImplicitTag(TagValue {
717//             class: TagClass::ContextSpecific,
718//             form: TagForm::Primitive,
719//             num: $num,
720//         }, $inner)
721//     };
722// }
723// pub(crate) use implicit_tag;
724
725// #[allow(unused_macros)]
726// macro_rules! explicit_tag {
727//     ($num:literal, $inner:expr) => {
728//         ExplicitTag(TagValue {
729//             class: TagClass::ContextSpecific,
730//             form: TagForm::Constructed,
731//             num: $num,
732//         }, ASN1($inner))
733//     };
734// }
735// pub(crate) use explicit_tag;
736
737}
verdict_parser/asn1/tag.rs

verdict_parser/asn1/
tag.rs
