Protection

Here, we define functions for QUIC packet packet protection.

include tls_msg
include collections

object protection = {

    module stream_data_protection(tls_id,tls) = {
        instance idx : unbounded_sequence
        instance arr : array(idx,stream_data)
    }

    module minip_protection(tls_id,tls) = {
        instance idx : unbounded_sequence
        instance arr : array(idx,stream_data)
    }

    module global_protection(tls_id,tls) = {
        instance idx : unbounded_sequence
        instance arr : array(idx,stream_data)

This is information we can extract from a packet whether it is protected or not.

        type header_info_quic = struct {
            hdr_long : bool,                   # true if long format
            hdr_type : type_bits,              # the type bits
            dcid : cid,                        # destination cid
            scid : cid,                        # source cid (for long format only)
            payload_length : stream_pos,       # payload lenght (for long format only)
            token_length : stream_pos,         # token lenght (for long format only)
            payload_length_pos : stream_pos,   # position in packet of length field, if present
            pkt_num_pos : stream_pos           # position in packet of sequence number
        }

Protect a packet, given the TLS session and the actual (not compressed) sequence number of the packet;

        action encrypt_quic(c:tls_id,seq:pkt_num,pkt:stream_data) returns (pkt:stream_data)

        action encrypt_zrtt_quic(c:tls_id,seq:pkt_num,pkt:stream_data) returns (pkt:stream_data)

Protect a packet, given the TLS session and the actual (not compressed) highest sequence number of any packet received so far. The latter is used to guess the real sequence number of the packet, which is needed to decrypt_quic the payload. This means that a significantly delayed packet might not be successfully decrypted, since we might not guess its full sequence number correctly. The return parameter ok is true if the packet is successfully decrypted. Note, unsuccessful decryption might indicate a stateless reset.

        action decrypt_quic(c:tls_id,seq:pkt_num,pkt:stream_data) returns (res:tls.decrypt_result)

        import action show_pkt_length(l:stream_pos)
        import action show_pkt(l:stream_data)

        implement encrypt_quic {

            var h := get_header_info(pkt,false);
            var level := get_level(pkt);
            var sample_size : stream_pos := tls.iv_size(c,level);
            var pnum_pos := h.pkt_num_pos;
            var pnum_len := get_pnum_len(pkt);
            var hdr_len := pnum_pos + pnum_len;

Tricky: before encrypting the payload, we need to adjust the length field so that it includes the AEAD checksum. Of course, we don't know what that actually is. Here we assume it is 16 bytes. Even worse, the length of the length field could grow. Here, we assume the length field format is always two bytes.

            if h.hdr_long {
                var new_len := to_var_int_16(h.payload_length+16);
                pkt := pkt.set(pnum_pos-2,new_len.value(0));
                pkt := pkt.set(pnum_pos-1,new_len.value(1));
            };

            var hdr  := pkt.segment(0,pnum_pos);
            var pnum := pkt.segment(pnum_pos,hdr_len);
            var pyld := pkt.segment(hdr_len,pkt.end);
            var auth := pkt.segment(0,hdr_len);
            var new_seq := get_pnum(pnum,0,pnum_len);
            new_seq := correct_pnum(seq,new_seq,pnum_len);
            pyld := tls.encrypt_aead(c,level,pyld,new_seq,auth);

call show_aead(level,pyld,new_seq,auth);

start l 3Computing the sample position is a bit tricky. First we assume the length of the pnum is 4, which means the offset of the sample withing the payload is 4 -pnum_len. However, if there are not enough bytes in the payload, we change it to payld.end - sample. Note, however, that we are using natural numbers, so if the position would be negative, it saturates to zero. This is consistent with the statement that you should never sample any bytes from the packet number itself. This leaves the possibility that there are not enough bytes to sample, that is, in the sample, there will be some trailing zeros. Nonetheless, the spec says that the sample size will never be larger than the smallest encrypted payload, so we should be OK.

            var pn_offset : stream_pos := 0;
            if h.hdr_long {
                pn_offset := hdr_len - pnum_pos;
            } else {
                pn_offset := 1 + 4;
            };

            var sample_pos : stream_pos :=  4 - pnum_len;  #- pnum_len;
            var new_pyld := pyld;
            if sample_pos + sample_size > pkt.end { #MC
                var diff := (sample_pos + sample_size) - pyld.end;
                var i : stream_pos := 0;
                while i < diff {
                    new_pyld := new_pyld.append(0x00);
                    i := i + 1
                };

sample_pos := pyld.end - sample_size #MC shift vs padding ? #[1] check with mcmillan vs maxime piraux

                pyld := new_pyld;  #[*2*]
            };

            var sample := pyld.segment(sample_pos,sample_pos+sample_size);
            var mask := stream_data.empty;
            mask := tls.encrypt_cipher(c,level,mask.resize(5,0),sample,false);
            var byte0_mask := bvand(mask.value(0), 0x0f if h.hdr_long else 0x1f);
            hdr := hdr.set(0,byte_xor(pkt.value(0),byte0_mask));
            pnum := stream_data_xor(pkt.segment(pnum_pos,pnum_pos+pnum_len),mask.segment(1,1+pnum_len));
            pkt := hdr.extend(pnum).extend(pyld);
        }

        implement encrypt_zrtt_quic {
            var h := get_header_info(pkt,false);
            var pkt_rtt := pkt.segment(h.payload_length,pkt.end);
            var pkt_init := pkt.segment(0,h.payload_length);
            var h_rtt := get_header_info(pkt_rtt,false);

---

            var level := get_level(pkt_init);
            var sample_size : stream_pos := tls.iv_size(c,level);
            var pnum_pos := h.pkt_num_pos;
            var pnum_len := get_pnum_len(pkt_init);
            var hdr_len := pnum_pos + pnum_len;

Tricky: before encrypting the payload, we need to adjust the length field so that it includes the AEAD checksum. Of course, we don't know what that actually is. Here we assume it is 16 bytes. Even worse, the length of the length field could grow. Here, we assume the length field format is always two bytes.

            if h.hdr_long {
                var new_len := to_var_int_16(h.payload_length-10); # 16 vs 10 -10 +16
                pkt_init := pkt_init.set(pnum_pos-2,new_len.value(0));
                pkt_init := pkt_init.set(pnum_pos-1,new_len.value(1));
            };

            var hdr  := pkt_init.segment(0,pnum_pos);
            var pnum := pkt_init.segment(pnum_pos,hdr_len);
            var pyld_i := pkt_init.segment(hdr_len,pkt.end);

            var auth := pkt_init.segment(0,hdr_len);
            var new_seq := get_pnum(pnum,0,pnum_len);
            new_seq := correct_pnum(seq,new_seq,pnum_len);
            pyld_i := tls.encrypt_aead(c,level,pyld_i,new_seq,auth);

start l 3Computing the sample position is a bit tricky. First we assume the length of the pnum is 4, which means the offset of the sample withing the payload is 4 -pnum_len. However, if there are not enough bytes in the payload, we change it to payld.end - sample. Note, however, that we are using natural numbers, so if the position would be negative, it saturates to zero. This is consistent with the statement that you should never sample any bytes from the packet number itself. This leaves the possibility that there are not enough bytes to sample, that is, in the sample, there will be some trailing zeros. Nonetheless, the spec says that the sample size will never be larger than the smallest encrypted payload, so we should be OK.

            var pn_offset : stream_pos := 0;
            if h.hdr_long {
                pn_offset := hdr_len - pnum_pos;
            } else {
                pn_offset := 1 + 4;
            };

            var sample_pos : stream_pos :=  4 - pnum_len;  #- pnum_len;
            var new_pyld := pyld_i;
            if sample_pos + sample_size > pkt_init.end { #MC
                var diff := (sample_pos + sample_size) - pyld_i.end;
                var i : stream_pos := 0;
                while i < diff {
                    new_pyld := new_pyld.append(0x00);
                    i := i + 1
                };

sample_pos := pyld.end - sample_size #MC shift vs padding ? #[1] check with mcmillan vs maxime piraux

                pyld_i := new_pyld;  #[*2*]
            };

            var sample := pyld_i.segment(sample_pos,sample_pos+sample_size);
            var mask := stream_data.empty;
            mask := tls.encrypt_cipher(c,level,mask.resize(5,0),sample,false);
            var byte0_mask := bvand(mask.value(0), 0x0f if h.hdr_long else 0x1f);
            hdr := hdr.set(0,byte_xor(pkt_init.value(0),byte0_mask));
            pnum := stream_data_xor(pkt_init.segment(pnum_pos,pnum_pos+pnum_len),mask.segment(1,1+pnum_len));
            pkt_init := hdr.extend(pnum).extend(pyld_i);

---

            var sample_size_rtt : stream_pos := tls.iv_size(c,1);
            var pnum_pos_rtt := h_rtt.pkt_num_pos;
            var pnum_len_rtt := get_pnum_len_b(pkt_rtt);
            var hdr_len_rtt := pnum_pos_rtt + pnum_len_rtt;

Tricky: before encrypting the payload, we need to adjust the length field so that it includes the AEAD checksum. Of course, we don't know what that actually is. Here we assume it is 16 bytes. Even worse, the length of the length field could grow. Here, we assume the length field format is always two bytes.

            if h_rtt.hdr_long {
                var new_len := to_var_int_16(h_rtt.payload_length+16);
                pkt_rtt := pkt_rtt.set(pnum_pos_rtt-2,new_len.value(0));
                pkt_rtt := pkt_rtt.set(pnum_pos_rtt-1,new_len.value(1));
            };

            var hdr_rtt  := pkt_rtt.segment(0,pnum_pos_rtt);
            var pnum_rtt := pkt_rtt.segment(pnum_pos_rtt,hdr_len_rtt);
            var pyld_rtt := pkt_rtt.segment(hdr_len_rtt,pkt_rtt.end);
            var auth_rtt := pkt_rtt.segment(0,hdr_len_rtt);
            var new_seq_rtt := get_pnum(pnum_rtt,0,pnum_len_rtt);
            new_seq_rtt := correct_pnum(seq,new_seq_rtt,pnum_len_rtt);
            pyld_rtt := tls.encrypt_aead(c,1,pyld_rtt,new_seq_rtt,auth_rtt);

start l 3Computing the sample position is a bit tricky. First we assume the length of the pnum is 4, which means the offset of the sample withing the payload is 4 -pnum_len. However, if there are not enough bytes in the payload, we change it to payld.end - sample. Note, however, that we are using natural numbers, so if the position would be negative, it saturates to zero. This is consistent with the statement that you should never sample any bytes from the packet number itself. This leaves the possibility that there are not enough bytes to sample, that is, in the sample, there will be some trailing zeros. Nonetheless, the spec says that the sample size will never be larger than the smallest encrypted payload, so we should be OK.

            var pn_offset_rtt : stream_pos := 0;
            if h_rtt.hdr_long {
                pn_offset_rtt := hdr_len_rtt - pnum_pos_rtt;
            } else {
                pn_offset_rtt := 1 + 4;
            };

            var sample_pos_rtt : stream_pos :=  4 - pnum_len_rtt;  #- pnum_len;
            var new_pyld_rtt := pyld_rtt;
            if sample_pos_rtt + sample_size_rtt > pkt_rtt.end  { #MC CHECK
                var diff := (sample_pos_rtt + sample_size_rtt) - pyld_rtt.end;
                var i : stream_pos := 0;
                while i < diff {
                    new_pyld_rtt := new_pyld_rtt.append(0x00);
                    i := i + 1
                };

check with mcmillan vs maxime piraux

                pyld_rtt := new_pyld_rtt;  #[*2*]
            };

            var sample_rtt := pyld_rtt.segment(sample_pos_rtt,sample_pos_rtt+sample_size_rtt);
            var mask_rtt := stream_data.empty;
            mask_rtt := tls.encrypt_cipher(c,1,mask_rtt.resize(5,0),sample_rtt,false); # TODO
            var byte0_mask_rtt := bvand(mask_rtt.value(0), 0x0f if h_rtt.hdr_long else 0x1f);
            hdr_rtt := hdr_rtt.set(0,byte_xor(pkt_rtt.value(0),byte0_mask_rtt));
            pnum_rtt := stream_data_xor(pkt_rtt.segment(pnum_pos_rtt,pnum_pos_rtt+pnum_len_rtt),mask_rtt.segment(1,1+pnum_len_rtt));
            pkt_rtt := hdr_rtt.extend(pnum_rtt).extend(pyld_rtt);

---

            pkt := pkt_init.extend(pkt_rtt);
        }

        implement decrypt_quic {
            var h := get_header_info(pkt,true);
            call show_header_debug_event(h);
            var level := get_level(pkt);
            if level = 1 & ~zrtt_pkt_set {
                zrtt_pkt_set := true;
                last_zrtt_pkt := pkt;
            };

            var sample_size := tls.iv_size(c,level);
            if ~zrtt_pkt_process & level = 1 {
                res.ok := false;
            } else if sample_size = 0 {
                res.ok := false;
            }
            else {
                var pnum_pos := h.pkt_num_pos; #+ h.token_length;
                var sample_pos := pnum_pos + 4; # + h.token_length;
                if sample_pos + sample_size > pkt.end {
                    sample_pos := pkt.end - sample_size
                };

                var sample := pkt.segment(sample_pos,sample_pos+sample_size);
                var pnum := pkt.segment(pnum_pos,pnum_pos+4);
                var mask := stream_data.empty;

tricky: this encrypts with the receiving cipher mask = header_protection(hp_key, sample)

                mask := tls.encrypt_cipher(c,level,mask.resize(5,0),sample,true);

if (packet[0] & 0x80) == 0x80: Long header: 4 bits masked packet[0] ^= mask[0] & 0x0f else: Short header: 5 bits masked packet[0] ^= mask[0] & 0x1f

                var byte0_mask := bvand(mask.value(0), 0x0f if h.hdr_long else 0x1f);

                var hdr := pkt.segment(0,pnum_pos);
                hdr := hdr.set(0,byte_xor(hdr.value(0),byte0_mask));

                var pnum_len := get_pnum_len_b(hdr);

                last_datagram_received_size := last_datagram_received_size +  h.payload_length + h.pkt_num_pos + pnum_len;

                call show_token_len_debug_event(pnum_len);
                pnum := stream_data_xor(pkt.segment(pnum_pos,pnum_pos+pnum_len),mask.segment(1,1+pnum_len));

                hdr := hdr.extend(pnum);
                var new_seq := get_pnum(pnum,0,pnum_len);
                new_seq := correct_pnum(seq,new_seq,pnum_len);
                var pyld := pkt.segment(pnum_pos+pnum_len,pkt.end);
                res := tls.decrypt_aead(c,level,pyld,new_seq,hdr); #
                if res.ok {

fix up the length field to account for removal of checksum

                    if h.hdr_long {
                        var new_len := to_var_int_16(h.payload_length-16);
                        hdr := hdr.resize(h.payload_length_pos,0);
                        hdr := hdr.extend(new_len);
                        hdr := hdr.extend(pnum);
                    };
                    res.payload := res.data;
                    res.data := hdr.extend(res.data);
                }
            }
        }

        action retry_integrity_tag(odcil: stream_pos, odcid: cid, pversion: version, dcil: stream_pos, dcid: cid, scil: stream_pos, scid: cid, token : stream_data, seq:pkt_num,h:stream_pos,b:bool) returns (cipher:stream_data)

        implement retry_integrity_tag {

TODO useless, call directly tls.compute_retry_integrity_tag

            var rt := tls.compute_retry_integrity_tag(
                                    odcil, cid_to_tls_id(odcid),
                                    pversion,
                                    dcil, cid_to_tls_id(dcid),
                                    scil, cid_to_tls_id(scid),
                                    token,seq,h,b);
            cipher := rt;
        }

        action cid_to_tls_id(c:cid) returns(res:tls_api.id) = {
        <<<
            res = c.val;
        >>>
        }

        action get_level(pkt:stream_data) returns (level:tls.level) = {
            if bvand(pkt.value(0),0x80) ~= 0 {
                var hdr_type := bvand(pkt.value(0),0x30); #  : type_bits :=  bfe[0][6](pkt.value(0)); #

call show_htype(hdr_type);

                if hdr_type = 0x00 | hdr_type = 0x30 { # | hdr_type = 0x20
                    level := 0;
                }
                else if hdr_type = 0x10 {

0RTT

                    level := 1;
                }
                else  { # if hdr_type = 0x20, TODO: other packet types
                    level := 2;
                }
            } else {
                level := 3;
            }
        }

FROM quic-tracker GetPacketSample

        action get_packet_sample(header:header_info_quic, packetByte: stream_data, pnum_pos:stream_pos,hdr_len:stream_pos,sample_size:stream_pos) returns (sample: stream_data) = {

var sample_length: stream_pos := 16;

            var pn_offset : stream_pos := 0;
            if header.hdr_long {
                pn_offset := hdr_len - pnum_pos;
            } else {
                pn_offset := 1 + 8; #should be length of dcid
            };
            sample := packetByte;
            var sample_offset := pn_offset + 4;
            if sample_offset + sample_size > packetByte.end {
                var diff := (sample_offset + sample_size) - packetByte.end;
                var i : stream_pos := 0;
                while i < diff {
                    sample := sample.append(0x00);
                i := i + 1
                };
            }
        }

This returns the header information of a packet, whether encrypted or not.

        action get_header_info(pkt:stream_data,decrypt_quic:bool) returns (h:header_info_quic) = {
            h.hdr_long := bvand(0x80,pkt.value(0)) ~= 0;
            h.hdr_type := bfe[0][6](pkt.value(0));
            if h.hdr_long {
                var dcil : stream_pos := bfe[0][7](pkt.value(5));
                h.dcid := bytes_to_cid(pkt.segment(6,6+dcil));
                var scil : stream_pos := bfe[0][7](pkt.value(6+dcil));
                h.scid := bytes_to_cid(pkt.segment(7+dcil,7+dcil+scil));
                if decrypt_quic {
                    client_initial_scil := scil;
                };
                var pos := 1 + 4 + 1 + dcil + 1 + scil; #7 + dcil + scil;
                var tlen : stream_pos := 0;
                var retry_token_len : stream_pos := 0;
                if bvand(h.hdr_type,0x30) = 0x00 {

Initial packet

                    tlen := get_var_int_len(pkt,pos);
                    retry_token_len := get_var_int(pkt,pos,tlen);
                    h.token_length := retry_token_len;
                    pos := pos + tlen + retry_token_len;
                } else {
                    h.token_length := 0;
                };
                var len := get_var_int_len(pkt,pos);
                h.payload_length := get_var_int(pkt,pos,len);
                h.payload_length_pos := pos;
                h.pkt_num_pos := pos + len;
            }
            else {

todo check if good for client test too

                if ~decrypt_quic {
                    h.dcid := bytes_to_cid(pkt.segment(1,1+client_initial_scil));
                    h.payload_length_pos := 1+client_initial_scil;
                    h.pkt_num_pos := 1+client_initial_scil;
                } else {
                    h.dcid := bytes_to_cid(pkt.segment(1,1+8));
                    h.payload_length_pos := 1+8;
                    h.pkt_num_pos := 1+8;
                }
            }
        }

This computes the full sequence number from the truncated version in the packet. It can fail if a packet is really old, in which case the packet won't decrypt_quic.

        action correct_pnum(last:pkt_num, pnum:pkt_num, pnum_len:stream_pos)
        returns (pnum:pkt_num) = {

TODO: for now we assume always 30-bit packet number format

            var diff : pkt_num := bfe[0][29](pnum - last);
            pnum := last + diff;
            if diff >= 0x20000000 {
                pnum := pnum - 0x40000000
            }
        }

Get the length of a packet number at position pos

        action get_pnum_len_b(pkt:stream_data) returns (pnum_len:stream_pos) = {
            <<<
            pnum_len = (pkt[0] & 0x3) + 1;
            >>>
        }

        action get_pnum_len(pkt:stream_data) returns (pnum_len:stream_pos) = {
            var len_minus_one : stream_pos := bfe[0][1](pkt.value(0));
            pnum_len := len_minus_one + 1;
        }

Given the length of the packet number, get the number it encodes.

        action get_pnum(pkt:stream_data,pnum_pos:stream_pos,pnum_len:stream_pos) returns (seq:pkt_num) = {
            var data := pkt.segment(pnum_pos,pnum_pos + pnum_len);
            seq := 0;
            var idx:stream_pos := 0;
            while idx < data.end {
                seq := 256 * seq + bfe[0][7](data.value(idx));
                idx := idx.next;
            }
        }

Get the length of a variable-length integer in a packet.

        action get_var_int_len(pkt:stream_data,pos:stream_pos) returns (len:stream_pos) = {
            var code := bvand(0xc0,pkt.value(pos));
            if code = 0 {
                len := 1;
            } else if code = 0x40 {
                len := 2;
            } else if code = 0x80 {
                len := 4;
            } else {
                len := 8;
            }
        }

Get the value of a variable-length integer at position pos, whose length is len.

        action get_var_int(pkt:stream_data,pos:stream_pos,len:stream_pos) returns (val:stream_pos) = {
            var idx:stream_pos := pos;
            val := 0;
            while idx < pos + len {
                var byte := pkt.value(idx);
                if idx = pos {
                    byte := bvand(byte,0x3f);
                };
                val := 256 * val + bfe[0][7](byte);
                idx := idx.next;
            }
        }

        action to_var_int_16(val:stream_pos) returns (bytes:stream_data) = {
            <<<
            bytes.push_back(0x40 | (val >> 8) & 0x3f);
            bytes.push_back(val & 0xff);
            >>>
        }

        action bytes_to_pos(b:byte) returns (val:stream_pos) = {
        <<<
        val = b;
        >>>
        }

        action pos_to_byte(b:stream_pos) returns (val:byte) = {
        <<<
        val = b;
        >>>
        }

        action bytes_to_cid(bytes:stream_data) returns (val:cid) = {
            <<<
            val.val = 0;
            for (unsigned i = 0; i < bytes.size(); i++)
                val.val = (val.val << 8) + bytes[i];
            >>>
        }

        action byte_xor(x:byte,y:byte) returns (z:byte) = {
            <<<
            z = x ^ y;
            >>>
        }

        action stream_data_xor(x:stream_data,y:stream_data) returns (x:stream_data) = {
            var idx := x.begin;
            while idx < x.end {
                x := x.set(idx,byte_xor(x.value(idx),y.value(idx)));
                idx := idx.next
            }
        }
        import action show_payload(ver:stream_data)
        import action show_token_len_debug_event(ver:stream_pos)
        import action show_header_debug_event(h:header_info_quic)
    }
}

Because of packet coalescing, we need a custom serializer and deserializer for protected packets. In particular, we need to look at the length field of the long form packets to find the packet boundaries within a datagram.

The serializer just concatenates the packets

object stream_prot_ser = {}

<<< member

    class `stream_prot_ser`;

>>>

<<< impl

    class `stream_prot_ser` : public ivy_binary_ser_128 {
    public:

        void open_list(int) {
        }

        virtual void  set(int128_t res) {
            setn(res,1);
        }
    };

>>>

The deserializer is tricker. It looks at the first byte of the packet to determine if it is a long or short packet. For long packets, it computes the total length based on the header bytes and the payload length field. This is a bit redundant with the above code, however this can't be helped as there is no way for the deserializer to have access to the ivy object.

object stream_prot_deser = {}

<<< member

    class `stream_prot_deser`;

>>>

<<< impl

    class `stream_prot_deser` : public ivy_binary_deser_128 {
        int data_remaining;
    public:
        stream_prot_deser(const std::vector<char> &inp) : ivy_binary_deser_128(inp) {
            data_remaining = inp.size();
        }

        void  get(int128_t &res) {
            getn(res,1);
        }

        unsigned char peek(unsigned p) {
            return more(p-pos+1) ? inp[p] : 0;
        }

        void open_list() {
            return;
        }

        bool open_list_elem() {
            bool res = data_remaining--> = 0;
            return res;
        }
        void close_list_elem() {
        }
    };

>>>