pub trait SecureSpecCombinator: SpecCombinator {
// Required methods
proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type);
proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>);
spec fn is_prefix_secure() -> bool;
proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>);
proof fn lemma_parse_length(&self, s: Seq<u8>);
spec fn is_productive(&self) -> bool;
proof fn lemma_parse_productive(&self, s: Seq<u8>);
// Provided methods
proof fn corollary_parse_surjective(&self, v: Self::Type) { ... }
fn corollary_serialize_injective(&self, v1: Self::Type, v2: Self::Type) { ... }
fn corollary_serialize_injective_contraposition(
&self,
v1: Self::Type,
v2: Self::Type,
) { ... }
fn corollary_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) { ... }
fn lemma_serialize_productive(&self, v: Self::Type) { ... }
}Expand description
Theorems and lemmas that must be proven for a combinator to be considered correct and secure.
Required Methods§
Sourceproof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
requires
self.requires(),self.wf(v)
==> self.spec_parse(self.spec_serialize(v))
== Some((self.spec_serialize(v).len() as int, v)),One of the top-level roundtrip properties It reads “if we serialize a (well-formed) value, then parsing the serialized bytes should give us the same value back.” If we somehow get a different value, it means that different high-level values can correspond to the same low-level representation, or put differently, the same byte sequences can be parsed into different values.
This property can be understood as
- injectivity of serialization: different values should serialize to different byte sequences
- surjectivity of parsing: every valid high-level value should associate with at least one low-level representation.
- correctness of parsing: given a correct serializer that produces some byte sequence from a value, the corresponding parser should be able to parse the byte sequence back to the same value (can lead to format-confusion attacks if not satisfied).
Sourceproof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
requires
self.requires(),self
.spec_parse(
buf,
) matches Some(
(n, v),
) ==> {
&&& self.wf(v)
&&& self.spec_serialize(v) == buf.take(n)
},One of the top-level roundtrip properties It reads “if we successfully parse a byte sequence, then serializing the parsed value should give us the same byte sequence back.” If we somehow get a different byte sequence, it means that different low-level representations can correspond to the same high-level value, or put differently, the same value can be serialized into different byte sequences.
This property can be understood as
- injectivity of parsing: different byte sequences should parse to different values (can lead to parser mallability attacks if not satisfied)
- correctness of serialization: given a correct parser that produces some value from a byte sequence, the corresponding serializer should be able to serialize the value back to the same byte sequence (up to the number of bytes consumed).
Sourcespec fn is_prefix_secure() -> bool
spec fn is_prefix_secure() -> bool
Like an associated constant, denotes whether the combinator is prefix-secure.
Sourceproof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
requires
self.requires(),Self::is_prefix_secure()
==> (self.spec_parse(s1) is Some ==> self.spec_parse(s1 + s2) == self.spec_parse(s1)),This prefix-secure lemma is used in the proof of the roundtrip properties for sequencing and repeating combinators.
Sourceproof fn lemma_parse_length(&self, s: Seq<u8>)
proof fn lemma_parse_length(&self, s: Seq<u8>)
requires
self.requires(),self.spec_parse(s) matches Some((n, _)) ==> 0 <= n <= s.len(),The parser-length lemma is used in the proof of the roundtrip properties and the prefix-secure lemma
Sourcespec fn is_productive(&self) -> bool
spec fn is_productive(&self) -> bool
Like an associated constant, denotes whether the combinator is productive
Sourceproof fn lemma_parse_productive(&self, s: Seq<u8>)
proof fn lemma_parse_productive(&self, s: Seq<u8>)
requires
self.requires(),self.is_productive() ==> (self.spec_parse(s) matches Some((n, _)) ==> n > 0),This lemma is used in the proof of the roundtrip properties for optional and unbounded repeating combinators.
Provided Methods§
Sourceproof fn corollary_parse_surjective(&self, v: Self::Type)
proof fn corollary_parse_surjective(&self, v: Self::Type)
requires
self.requires(),self.wf(v),exists |b: Seq<u8>| #[trigger] self.spec_parse(b) matches Some((_, v_)) && v_ == v,Followed from theorem_serialize_parse_roundtrip
Sourceproof fn corollary_serialize_injective(&self, v1: Self::Type, v2: Self::Type)
proof fn corollary_serialize_injective(&self, v1: Self::Type, v2: Self::Type)
requires
self.requires(),self.wf(v1) && self.wf(v2)
==> (self.spec_serialize(v1) == self.spec_serialize(v2) ==> v1 == v2),Followed from theorem_serialize_parse_roundtrip
Sourceproof fn corollary_serialize_injective_contraposition(
&self,
v1: Self::Type,
v2: Self::Type,
)
proof fn corollary_serialize_injective_contraposition( &self, v1: Self::Type, v2: Self::Type, )
requires
self.requires(),self.wf(v1) && self.wf(v2)
==> (v1 != v2 ==> self.spec_serialize(v1) != self.spec_serialize(v2)),Followed from theorem_serialize_parse_roundtrip
Sourceproof fn corollary_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)
proof fn corollary_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)
requires
self.requires(),self
.spec_parse(
buf1,
) matches Some(
(n1, v1),
) ==> self
.spec_parse(
buf2,
) matches Some((n2, v2)) ==> v1 == v2 ==> buf1.take(n1) == buf2.take(n2),Followed from theorem_parse_serialize_roundtrip
Sourceproof fn lemma_serialize_productive(&self, v: Self::Type)
proof fn lemma_serialize_productive(&self, v: Self::Type)
requires
self.requires(),self.wf(v),self.is_productive() ==> self.spec_serialize(v).len() > 0,This lemma is used in the proof of the roundtrip properties for optional and unbounded repeating combinators.
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Implementations on Foreign Types§
Source§impl<C: SecureSpecCombinator> SecureSpecCombinator for &C
impl<C: SecureSpecCombinator> SecureSpecCombinator for &C
Source§open spec fn is_prefix_secure() -> bool
open spec fn is_prefix_secure() -> bool
{ C::is_prefix_secure() }Source§open spec fn is_productive(&self) -> bool
open spec fn is_productive(&self) -> bool
{ (*self).is_productive() }Source§proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
Source§proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
Source§proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
Source§proof fn lemma_parse_length(&self, s: Seq<u8>)
proof fn lemma_parse_length(&self, s: Seq<u8>)
Source§proof fn lemma_parse_productive(&self, s: Seq<u8>)
proof fn lemma_parse_productive(&self, s: Seq<u8>)
Source§impl<C: SecureSpecCombinator> SecureSpecCombinator for Box<C>
impl<C: SecureSpecCombinator> SecureSpecCombinator for Box<C>
Source§open spec fn is_prefix_secure() -> bool
open spec fn is_prefix_secure() -> bool
{ C::is_prefix_secure() }Source§open spec fn is_productive(&self) -> bool
open spec fn is_productive(&self) -> bool
{ (**self).is_productive() }Source§proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
Source§proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
Source§proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
Source§proof fn lemma_parse_length(&self, s: Seq<u8>)
proof fn lemma_parse_length(&self, s: Seq<u8>)
Source§proof fn lemma_parse_productive(&self, s: Seq<u8>)
proof fn lemma_parse_productive(&self, s: Seq<u8>)
Source§impl<Fst: SecureSpecCombinator, Snd: SecureSpecCombinator> SecureSpecCombinator for (Fst, Snd)
impl<Fst: SecureSpecCombinator, Snd: SecureSpecCombinator> SecureSpecCombinator for (Fst, Snd)
Source§proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
Source§proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
Source§open spec fn is_prefix_secure() -> bool
open spec fn is_prefix_secure() -> bool
{ Fst::is_prefix_secure() && Snd::is_prefix_secure() }Source§proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>)
proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>)
Source§proof fn lemma_parse_length(&self, s: Seq<u8>)
proof fn lemma_parse_length(&self, s: Seq<u8>)
Source§open spec fn is_productive(&self) -> bool
open spec fn is_productive(&self) -> bool
{ Pair::spec_new(self.0, |r: Fst::Type| self.1).is_productive() }