include collections
include order
include quic_stream
include quic_transport_error_code
include quic_h3_error_code
The frame protocol¤
The frame protocol is defined by a sequence of frame events. This protocol is layered on the packet protocol, such that each packet event contains a sub-sequence of the frame events.
The frame events are subdivided into variants called frame types.
For each frame type, we define an event handle corresponding
to the generation of a frame and its transfer to the packet protocol
for transmission. Frame events effect the protocol state by
enqueueing frames to be encapsulated into packets. The effect of
this is that frame and packet events are interleaved, such that the
frames in each packet occur immediately before the packet event in
the same order in which they occur in the packet payload. TODO:
While this ordering seems sensible from a semantic point of view,
implementations might transmit frames out of order. Requiring
frame events to be in order might complicate a modular proof of the
implementation.
Each frame has an encryption level (which is the same as the packet type it will be encapsulated in). The enryption level determines the keys used to protect to protect that packet payload. Only frames of the same encryption level may be encapsulated in the same packet (however, multiple packets may be concatenated in a single UDP datagram). This requirement is enforced by requiring that every frame queue contains only frames of the same encryption level. The frame handler for each type enforces this condition.
Data structures¤
WARNING Order define tag used in quic_ser & quic_deser
object frame = {
type this
object ping = {
variant this of frame = struct {
}
}
object ack = {
object range = {
type this = struct {
gap : pkt_num, # gap, or zero for first range
ranges : pkt_num # number of packets in range - 1
}
instance idx : unbounded_sequence
instance arr : array(idx,this)
}
variant this of frame = struct {
largest_acked : pkt_num, # largest acknowledged packet number
ack_delay : microseconds, # delay of largest acked packet
ack_ranges : range.arr # ack ranges
}
}
object ack_ecn = {
object range = {
type this = struct {
gap : pkt_num, # gap, or zero for first range
ranges : pkt_num # number of packets in range - 1
}
instance idx : unbounded_sequence
instance arr : array(idx,this)
}
object ecn = { type this = struct { ect0 : pkt_num, # total number of packets received with the ECT(0) ect1 : pkt_num, # total number of packets received with the ECT(1) ecn_ce : pkt_num # total number of packets received with the CE codepoint } instance idx : unbounded_sequence instance arr : array(idx,this) }
Ack frames are a variant of frame
variant this of frame = struct {
largest_acked : pkt_num, # largest acknowledged packet number
ack_delay : microseconds, # delay of largest acked packet
ack_ranges : range.arr, # ack ranges
ecnp : bool, # is this the final offset
ect0 : pkt_num, # total number of packets received with the ECT(0)
ect1 : pkt_num, # total number of packets received with the ECT(1)
ecn_ce : pkt_num # total number of packets received with the CE codepoint
}
}
object rst_stream = {
variant this of frame = struct {
id : stream_id, # id of stream being reset
err_code : error_code, # the error code
final_offset : stream_pos # position of the end of the stream
}
}
object stop_sending = {
variant this of frame = struct {
id : stream_id, # the stream id
err_code : error_code # the error code
}
}
object crypto = {
variant this of frame = struct {
offset : stream_pos, # the stream offset (zero if ~off)
length : stream_pos, # length of the data
data : stream_data # the stream data
}
}
object new_token = {
variant this of frame = struct {
length : stream_pos, # length of the token
data : stream_data # the token
}
}
object stream = {
variant this of frame = struct {
off : bool, # is there an offset field
len : bool, # is there a length field
fin : bool, # is this the final offset
id : stream_id, # the stream ID
offset : stream_pos, # the stream offset (zero if ~off)
length : stream_pos, # length of the data
data : stream_data # the stream data
}
}
object max_data = {
variant this of frame = struct {
pos : stream_pos # max number of bytes
}
}
object max_stream_data = {
variant this of frame = struct {
id : stream_id, # the stream id
pos : stream_pos # max number of bytes
}
}
object max_streams = { # TODO: handle cases of MAX_STREAMS for bidi and uni
variant this of frame = struct {
id : stream_id # maximum stream id
}
}
object max_streams_bidi = { # TODO: handle cases of MAX_STREAMS for bidi and uni
variant this of frame = struct {
id : stream_id # maximum stream id
}
}
object data_blocked = {
variant this of frame = struct {
pos : stream_pos # max number of bytes
}
}
object stream_data_blocked = {
variant this of frame = struct {
id : stream_id, # the stream id
pos : stream_pos # max number of bytes
}
}
object streams_blocked = { # TODO: handle bidi and uni cases => create streams_blocked_uni and streams_blocked_bidi + serializer
variant this of frame = struct {
id : cid # the stream id (we use cid for the 16 bytes)
}
}
object streams_blocked_bidi = { # TODO: handle bidi and uni cases => create streams_blocked_uni and streams_blocked_bidi + serializer
variant this of frame = struct {
id : cid # the stream id (we use cid for the 16 bytes)
}
}
object new_connection_id = {
variant this of frame = struct {
seq_num : cid_seq, # the sequence number of the new cid
retire_prior_to : cid_seq, # retire seq nums prior to this
length : cid_length, # the length of the new cid in bytes
scid : cid, # the new cid
token : reset_token # the stateless reset token
}
}
object retire_connection_id = {
variant this of frame = struct {
seq_num : cid_seq # the sequence number of the new cid
}
}
object path_challenge = {
variant this of frame = struct {
data : stream_data # 8-byte payload
}
}
object path_response = {
variant this of frame = struct {
data : stream_data # 8-byte payload
}
}
object connection_close = {
variant this of frame = struct {
err_code : error_code, # the error code
frame_type : error_code, # TODO: not the real type
reason_phrase_length : stream_pos, # number of bytes in reason phrase
reason_phrase : stream_data # bytes of reason phrase
}
}
object application_close = {
variant this of frame = struct {
err_code : error_code, # the error code
reason_phrase_length : stream_pos, # number of bytes in reason phrase
reason_phrase : stream_data # bytes of reason phrase
}
}
object handshake_done = {
variant this of frame = struct {
}
}
(0xaf) https://tools.ietf.org/html/draft-iyengar-quic-delayed-ack-02
object ack_frequency = { # TODO could be moved BUT need to refactor the deser/ser in csq
variant this of frame = struct {
seq_num : pkt_num, # the sequence number
ack_eliciting_threshold : stream_pos, #maximum number of ack-eliciting packets after which the receiver sends an acknowledgement.
request_max_ack_delay : microseconds,
reordering_threshold : stream_pos
}
}
object immediate_ack = {
variant this of frame = struct {
}
}
object unknown_frame = {
variant this of frame = struct {
}
}
object malicious_frame = {
variant this of frame = struct {
data: stream_data
}
}
} }
instance idx : unbounded_sequence
instance arr : array(idx,this)
}
The generic event for frames is specialized for each frame type. Its arguments are:
f: the frame contentsscid: the source aiddcid: the destination aide: the encryption levelseq_num: the packet number where the frame is
object frame = {
...
action handle(f:this,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num) = {
require false; # this generic action should never be called
}
}
Specification state¤
-
For each aid C,and stream id S,
stream_seen(C,S)indicates that a stream has been opened by aid C. -
For each aid C,and stream id S,
max_stream_data_val(C,S)indicates the maximum number of bytes that may be sent on stream id S to C. -
For each aid C,and stream id S,
max_stream_data_set(C,S)indicates the maximum number of bytes that may be sent on stream id S to C has been set. -
For each aid C,
max_data_val(C,S)indicates the maximum total number of bytes that may be sent on all streams to C. -
For each aid C,
max_data_set(C,S)indicates the maximum total number of bytes that may be sent on all streams to C has been set. -
For each aid C,and stream id S,
stream_length(C,S)indicates the length of the stream data transmitted in QUIC packets on stream id S to cid C. The length is the least stream position greater than the position of all bytes transmitted. Note this may be less than the length of the application data, but may not be greater. -
For aid C,and stream id S,
stream_finished(C,S)indicates that the stream transmitted to C on stream id S is finished (that is, a FIN frame has been sent). -
For each aid C,and stream id S,
stream_reset(C,S)indicates that the stream transmitted to C on stream id S is reset (that is, a RESET_STREAM frame has been sent). -
For each aid C,and stream kind K,
max_stream_set(C,K)indicates that the maximum stream id has been declared. -
For each aid C,and stream kind K,
max_stream(E,C,K)indicates the declared maximum stream id. -
The queued frames at aid
Care represented byqueued_frames(C)and are initially empty. -
The function queued_level(C) gives the packet type associated with the currently queued frames for aid C
TODO: Currently we can only queue frames of the same packet type, We should have a separate frame queue for each packet type.
-
The relation
queued_non_probing(C)indicates that one of the queued frames at aidCcontains a non-probing frame. This is a frame other than path challenge, new connection id and padding. -
The relation
queued_non_ack(C)indicates that one or more of the queued frames at aidCis not an ACK frame with padding. -
The relation
queued_close(C)indicates that one or more of the queued frames at aidCis a CONNECTION_CLOSE or APPLICATION_CLOSE frame. -
The function num_queued_frames(C:cid) gives the number of frames queue at aid
C. -
The predicate
path_challenge_pending(C,D)that a path challenge has been sent to aid C with data D, and has not yet been responded to. QUESTION: should path responses be resent, or should the client wait for a resent path challenge? -
The function
conn_total_data(C)represents the total number of stream bytes received by aidC.
Hamid
- The relation queued_ack_eliciting(C) indicates that one or more of the queued
frames at aid C is an ACK eliciting frame, i.e. according to draft 24, frames other than ACK, PADDING, CONNECTION_CLOSE
Hamid
chris
- the function queued_level_type(C:cid,T:quic_packet_type) : frame.arr is used to queue frames a separate frame queue for each packet type. TODO
- the relation send_retire_cid(C:cid,S:stream_id) is used to say that the next frame should be a retire_CID frame
- the function `max_rtp_num(C:cid) : cid_seq``is used to get the maximum retire_prior_to field in new_cid frame
- STREAM frame retransmission: 13.3. Retransmission of Information
* Application data sent in STREAM frames is retransmitted in new
STREAM frames unless the endpoint has sent a RESET_STREAM for that
stream. Once an endpoint sends a RESET_STREAM frame, no further
STREAM frames are needed.
We can consider that a STREAM frame is retransmitted if we receive a Frame twice with the same
information. For that we use more or less the same approach than Copy-On-Write for memory
We use a reference count (count_stream_frame) for each STREAM frame that we get. 0 meaning no reference, 1 = received once, ect
If count_stream_frame > 1 => this frame has been retransmitted and stream_frame_restransmitted is true
- RESET_STREAM frame retransmission = same approach
* Cancellation of stream transmission, as carried in a RESET_STREAM
frame, is sent until acknowledged or until all stream data is
acknowledged by the peer (that is, either the "Reset Recvd" or
"Data Recvd" state is reached on the sending part of the stream).
The content of a RESET_STREAM frame MUST NOT change when it is
sent again.
- STREAM_DATA_BLOCKED frame retransmission = same approach
* Blocked signals are carried in DATA_BLOCKED, STREAM_DATA_BLOCKED,
and STREAMS_BLOCKED frames. DATA_BLOCKED frames have connection
scope, STREAM_DATA_BLOCKED frames have stream scope, and
STREAMS_BLOCKED frames are scoped to a specific stream type. New
frames are sent if packets containing the most recent frame for a
scope is lost, but only while the endpoint is blocked on the
corresponding limit. These frames always include the limit that
is causing blocking at the time that they are transmitted.
- first_ack_freq_received return true if we received the first ack_freq frame
- last_ack_freq_seq(C:cid) return the seqnum associated to the last ack_frequency
frame received
chris
relation stream_seen(C:cid,S:stream_id)
function max_stream_data_val(C:cid,S:stream_id) : stream_pos
relation max_stream_data_set(C:cid,S:stream_id)
function max_data_val(C:cid) : stream_pos
relation max_data_set(C:cid)
function stream_length(C:cid,S:stream_id) : stream_pos
relation stream_finished(C:cid,S:stream_id)
relation stream_reset(C:cid,S:stream_id)
relation max_stream_set(C:cid,K:stream_kind)
function max_stream(C:cid,K:stream_kind) : stream_id
function queued_frames(C:cid) : frame.arr
function queued_frames_rtt(C:cid) : frame.arr
function queued_level(C:cid) : quic_packet_type
function queued_level_rtt(C:cid) : quic_packet_type
relation queued_non_probing(C:cid)
relation queued_non_ack(C:cid)
relation queued_challenge(C:cid)
relation queued_close(C:cid)
function num_queued_frames(C:cid) : frame.idx
function num_queued_frames_rtt(C:cid) : frame.idx
relation path_challenge_pending(C:cid,D:stream_data)
relation path_challenge_sent(C:cid)
function conn_total_data(C:cid) : stream_pos
relation queued_ack_eliciting(C:cid)
relation queued_ack_eliciting_pkt(C:stream_pos) # TODO
function num_ack_eliciting_pkt : stream_pos
function num_ack_pkt : stream_pos
import action show_num_ack_eliciting_pkt(s:stream_pos)
import action show_num_ack_pkt(s:stream_pos)
chris
function queued_level_type(C:cid,T:quic_packet_type) : frame.arr
relation send_retire_cid(C:cid)
function max_rtp_num(C:cid) : cid_seq
function count_stream_frame(I:stream_id,O:stream_pos,
L:stream_pos,D:stream_data) : stream_pos
relation stream_frame_restransmitted(S:stream_id)
function count_reset_frame(I:stream_id,E:error_code,O:stream_pos) : stream_pos
relation reset_frame_restransmitted(S:stream_id)
function count_sdb_frame(I:stream_id,O:stream_pos) : stream_pos
relation sdb_frame_restransmitted(S:stream_id)
function first_ack_freq_received : bool
function largest_unacked : pkt_num
function largest_acked : pkt_num
function unreported_missing : pkt_num
function last_ack_freq_seq(C:cid) : pkt_num
function count_newcid_frame(I:cid_seq,O:cid_seq, L:cid_length,D:cid,T:reset_token) : stream_pos
function count_rcid_frame(I:cid_seq) : stream_pos
relation connection_closed
relation handshake_done_send # TODO add src-endpoints
relation handshake_done_recv # TODO add src-endpoints
function last_cid_seq(C:cid):cid_seq
function first_zrtt_pkt : cid
relation zrtt_pkt_update
relation is_stream_limit_test
relation is_crypto_limit_test
relation stop_sending_in_bad_state
relation newly_acked(S:stream_pos)
function ack_eliciting_threshold_val(C:cid) : stream_pos
function current_ack_frequency(C:cid) : stream_pos
function ack_eliciting_threshold_current_val(C:cid) : stream_pos
function ack_out_of_order_val(C:cid) : stream_pos
function ack_out_of_order_current_val(C:cid) : stream_pos
after init {
stream_seen(C,S) := false;
stream_length(C,S) := 0;
max_stream_data_set(C,S) := false;
max_data_set(C) := false;
stream_finished(C,S) := false;
stream_reset(C,S) := false;
queued_non_probing(C) := false;
queued_non_ack(C) := false;
queued_close(C) := false;
path_challenge_pending(C,D) := false;
queued_ack_eliciting(C) := false;
max_rtp_num(C) := 0;
send_retire_cid(C) := false;
count_stream_frame(I,O,L,D) := 0; #B,J,F,
stream_frame_restransmitted(S) := false;
count_reset_frame(I,E,O) := 0;
reset_frame_restransmitted(S) := false;
count_sdb_frame(I,O) := 0;
sdb_frame_restransmitted(S) := false;
stop_sending_in_bad_state := false;
first_ack_freq_received := true;
last_ack_freq_seq(C) := 0;
connection_closed := false;
handshake_done_send := false;
handshake_done_recv := false;
is_stream_limit_test := false;
is_crypto_limit_test := false;
last_cid_seq(C) := 0;
zrtt_pkt_update := false;
newly_acked(S) := true;
queued_ack_eliciting_pkt(C) := false;
ack_eliciting_threshold_val(C) := 0;
ack_eliciting_threshold_current_val(C) := 0;
ack_out_of_order_val(C) := 1;
ack_out_of_order_current_val(C) := 0;
num_ack_eliciting_pkt := 0;
num_ack_pkt := 0;
}
ACK event¤
The set of packet numbers acknowledged by an ACK frame is determined
by the largest_ack field and the ack_blocks field. Each ACK
block acknowledges packet numbers in the inclusive range [last - gap, last -gap - blocks]<code> where </code>gap<code> and </code>ranges are the fields of the ACK
range and last is largest_ack minus the sum of gap + ranges
for all the previous ack ranges.
The gap field for the first ack range is always zero and is not
present in the low-level syntax.
Requirements:
- Every acknowledged packet must have been sent by the destination endpoint [1].
- Keys must be established for the given encryption level [4].
Effects:
- The acknowledged packets are recorded in the relation
acked_pkt(C,N)whereCis the source of the acknowledged packet (not of the ACK) andNis the packet number [2]. -
The greatest acked packet is also tracked in
max_acked(C,e)[3] -
If a packet with a connection_close frame of either type is acknowledged the sending aid enters the draining state. Note that observing the ack of a connection close frame is the only way we can detect that it was received.
Temporary
use this to enforce new acks in testing. Without this, too many duplicate acks would be generated.
var force_new_ack : bool
import action is_generating(b:bool)
import action is_ack_frequency_respected(b:bool)
object frame = {
...
object ack = {
...
action handle(f:frame.ack,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
if ~_generating {
call is_ack_frequency_respected(num_ack_eliciting_pkt > ack_eliciting_threshold_val(scid));
call is_ack_frequency_respected(num_ack_eliciting_pkt > ack_eliciting_threshold_val(dcid));
num_ack_eliciting_pkt := 0;
}
require connected(dcid) & connected_to(dcid) = scid;
if _generating {
require ~(e = quic_packet_type.initial) & ~(e = quic_packet_type.handshake); #& ~(e = quic_packet_type.handshake)
require ~conn_closed(scid);
Scaling in this fashion allows for a larger range of values with a shorter encoding at the cost of lower resolution. Because the receiver doesn't use the ACK Delay for Initial and Handshake packets, a sender SHOULD send a value of 0. TODO
};
require e = quic_packet_type.handshake -> established_handshake_keys(scid); # [4]
require e = quic_packet_type.one_rtt -> established_1rtt_keys(scid); # [4]
require ~(e = quic_packet_type.version_negociation) & ~(e = quic_packet_type.retry) & ~(e = quic_packet_type.zero_rtt);
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
var idx : frame.ack.range.idx := 0;
var last := f.largest_acked;
if max_acked(dcid,e) < last {
max_acked(dcid,e) := last; # [3]
};
call show_ack_eliciting_threshold_current_val(ack_eliciting_threshold_current_val(scid));
call show_ack_eliciting_threshold_current_val(ack_eliciting_threshold_current_val(dcid));
call show_ack_eliciting_threshold_val(ack_eliciting_threshold_val(scid));
call show_ack_eliciting_threshold_val(ack_eliciting_threshold_val(dcid));
require f.ack_ranges.end > 0;
var some_new_ack := false;
while idx < f.ack_ranges.end {
var ack_range := f.ack_ranges.value(idx);
require idx > 0 -> ack_range.gap < last - 1;
var upper := last - ((ack_range.gap+2) if idx > 0 else 0);
require ack_range.ranges <= upper;
last := upper - ack_range.ranges;
var jdx := last;
while jdx <= upper {
require sent_pkt(dcid,e,jdx); # [1]
if pkt_has_close(dcid,e,jdx) {
conn_draining(scid) := true # [5]
};
if ~acked_pkt(dcid,e,jdx) {
some_new_ack := true;
call show_ack_generated;
ack_eliciting_threshold_current_val(dcid) := 0;
};
acked_pkt(dcid,e,jdx) := true;
jdx := jdx + 1
};
idx := idx.next;
};
if _generating {
require some_new_ack;
require f.largest_acked = max_acked(dcid,e);
call show_ack_generated;
}
...
if ~_generating {
call on_ack_received(dst_endpoint,f.largest_acked, f.ack_delay,e);
}
force_new_ack := false;
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
import action show_local_delay_ack(val:microseconds, val2:microseconds)
import action show_ack_generated
import action show_ack_eliciting_threshold_current_val(val:stream_pos)
import action show_ack_eliciting_threshold_val(val:stream_pos)
object frame = {
...
object ack_ecn = {
...
action handle(f:frame.ack_ecn,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
if _generating {
require ~(e = quic_packet_type.initial) & ~(e = quic_packet_type.handshake); #& ~(e = quic_packet_type.handshake)
};
require e = quic_packet_type.handshake -> established_handshake_keys(scid); # [4]
require e = quic_packet_type.one_rtt -> established_1rtt_keys(scid); # [4]
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
var idx : frame.ack_ecn.range.idx := 0;
var last := f.largest_acked;
if max_acked(dcid,e) < last {
max_acked(dcid,e) := last; # [3]
};
require f.ack_ranges.end > 0;
var some_new_ack := false;
while idx < f.ack_ranges.end {
var ack_range := f.ack_ranges.value(idx);
require idx > 0 -> ack_range.gap < last - 1;
var upper := last - ((ack_range.gap+2) if idx > 0 else 0);
require ack_range.ranges <= upper;
last := upper - ack_range.ranges;
var jdx := last;
while jdx <= upper {
require sent_pkt(dcid,e,jdx); # [1]
if pkt_has_close(dcid,e,jdx) {
conn_draining(scid) := true # [5]
};
if ~acked_pkt(dcid,e,jdx) {
some_new_ack := true;
};
acked_pkt(dcid,e,jdx) := true;
jdx := jdx + 1
};
idx := idx.next;
};
if _generating {
require some_new_ack;
}
...
force_new_ack := false;
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
STREAM event¤
STREAM frames carry stream data.
Requirements:
-
The upper bound of the stream frame may not exceed the current value of
max_stream_data_valfor the given destination and cid, if it has been set [2]. -
If the stream is finished, the the frame offset plus length must not exceed the stream length [5].
-
The stream id must be less than or equal to the max stream id for the kind of the stream [6].
-
The stream must not have been reset [7].
-
The connection must not have been closed by the source endpoint [8].
-
The connection id must have been seen at the source [9] and the connection between source and destination must not be initializing [10].
-
The 1rtt keys have been established [11].
-
If the sender as reset the stream to a given length, then the end of the stream frame data must not exceed the reset length [13].
Effects:
-
If the stream has not been seen before, and if the
initial_max_stream_datatransport parameter has been set, then themax_stream_data_valvalue is set to the value of theinitial_max_stream_datatransport parameter [3]. -
The length of the stream is updated.
-
If the fin bit is set, the stream is marked as finished.
-
The total amount of data received on the connection is updated. Note this reflects the total of the observed length of all streams, including any unreceived gaps.
object frame = { # TODO cleanup
...
object stream = {
...
action handle(f:frame.stream,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
if (~zero_rtt_allowed | zero_rtt_sent) & ~(e = quic_packet_type.zero_rtt) {
require tls_handshake_finished;
require (connected(dcid) & connected_to(dcid) = scid); # | (e = quic_packet_type.zero_rtt & established_0rtt_keys(scid)); #e = quic_packet_type.zero_rtt &
require (e = quic_packet_type.one_rtt & established_1rtt_keys(scid)); # | (e = quic_packet_type.zero_rtt & established_0rtt_keys(scid)); # | e = quic_packet_type.zero_rtt | e = quic_packet_type.zero_rtt & established_0rtt_keys(scid)
} else {
require (e = quic_packet_type.one_rtt & established_1rtt_keys(scid)) | (e = quic_packet_type.zero_rtt & ~established_1rtt_keys(scid));
}
if ~zero_rtt_allowed | zero_rtt_sent {
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
}
[11] (e = quic_packet_type.zero_rtt & established_0rtt_keys(scid) require e = quic_packet_type.zero_rtt -> established_0rtt_keys(scid); # [11] require e = quic_packet_type.one_rtt -> established_1rtt_keys(scid);
require ~conn_closed(scid); # [8]
var offset := f.offset if f.off else 0;
require ((offset) + (f.length)) <= stream_app_data_end(dcid,f.id);
require f.data = stream_app_data(dcid,f.id).segment(offset,offset+f.length); # TODO
require f.fin <-> (stream_app_data_finished(dcid,f.id) & offset+f.length = stream_app_data_end(dcid,f.id));
var kind := get_stream_kind(f.id);
if (~zero_rtt_allowed | zero_rtt_sent) {
require conn_seen(scid); # [9]
}
if _generating {
};
require stream_reset(dcid,f.id) ->
((offset) + (f.length)) <= stream_length(dcid,f.id); # [13]
if ~zero_rtt_allowed | zero_rtt_sent { # | ~_generating
require stream_id_allowed(dcid,f.id,e); # [6]
}
else if _generating {
require f.id = 4; # f.id = 8 |f.id = 4 |
}
...
stream_seen(scid,f.id) := true;
var offset := f.offset if f.off else 0;
var length := offset + f.length;
if stream_length(dcid,f.id) < length {
conn_total_data(dcid) := conn_total_data(dcid) +
(length - stream_length(dcid,f.id)); # [12]
stream_length(dcid,f.id) := length
};
if f.fin {
stream_finished(dcid,f.id) := true;
};
if (~zero_rtt_allowed | zero_rtt_sent) & ~(e = quic_packet_type.zero_rtt) { #TODO
call enqueue_frame(scid,f,e,false,seq_num);
} else {
first_zrtt_pkt := dcid;
call enqueue_frame_rtt(scid,f,e,false);
}
}
}
}
CRYPTO event¤
CRYPTO frames carry crypto handshake data, that is, TLS records.
Requirements:
- The connection must not have been closed by the source endpoint [1].
- The bytes are present in
crypto_data[2]. chris -
It can be sent in all packet types except 0-RTT. [4] (implicit, needed ?) chris Effects:
-
The length of the crypto stream and the present bits are updated. [3]
object frame = {
...
object crypto = {
...
action handle(f:frame.crypto,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require ~conn_closed(scid); # [1]
require e ~= quic_packet_type.zero_rtt; # [4]
require ((f.offset) + (f.length)) <= crypto_data_end(scid,e); # [2]
require f.data = crypto_data(scid,e).segment(f.offset,f.offset+f.length); # [2]
...
var length := f.offset + f.length;
if crypto_length(scid,e) < length {
crypto_length(scid,e) := length; # [3]
};
var idx := f.offset;
while idx < f.offset + f.length {
crypto_data_present(scid,e,idx) := true; # [3]
idx := idx.next
};
call enqueue_frame(scid,f,e,false,seq_num);
if e = quic_packet_type.handshake {
established_1rtt_keys(scid) := true;
}
}
}
}
import action show_crypto_length(pkt:stream_pos)
RESET_STREAM events¤
RESET_STREAM frames cause an identified stream to be abruptly terminated, meaning the no further transmissions (or retransmissions) will be sent for this stream and the receiver may ignore any data previously transmitted.
Requirements:
- Stream id must has been created to be reset [8]. (FSM)
- Stream id must not exceed maximim stream id for the stream kind [4].
-
Question
Can a previously reset stream be reset?
- The final stream position may not be lesser than that of any previous stream frame for the same stream id [1].
- The connection must not have been closed by the source endpoint [5].
- The encryption level must be 0rtt or 1rtt [6].
- If stream was previously reset or finished, final offset must be same [7].
Effects:
- The specified stream id is marked as reset [2].
- The stream length is set to the given final offset [3].
Question: Where is it written that reset stream frames cannot occur in initial or handshake packets?
object frame = { ...
object rst_stream = { ...
action handle(f:frame.rst_stream,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid); # [6]
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require ~conn_closed(scid); # [5]
require connected(scid) & connected_to(scid) = dcid;
require stream_length(dcid,f.id) <= f.final_offset; # [1]
if _generating {
};
require (stream_reset(dcid,f.id) | stream_finished(dcid,f.id)) -> stream_length(dcid,f.id) = f.final_offset;
stream_reset(dcid,f.id) := true; # [2]
stream_length(dcid,f.id) := f.final_offset; #[3]
require stream_id_allowed(dcid,f.id,e); # [4]
...
if ~_generating {
call handle_transport_error(f.err_code);
call handle_h3_error(f.err_code);
};
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
STOP_SENDING event¤
STOP_SENDING frames are sent by the receiver of s stream to indicate that stream data is being ignored and it should stop sending.
Requirements:
- Receiving a STOP_SENDING frame for a locally-initiated stream that has not yet been created MUST be treated as a connection error of type STREAM_STATE_ERROR.. [8] (FSM)
- Stream id must not exceed maximim stream id for the stream kind [4].
-
Question
Can a previously reset stream be reset?
- The connection must not have been closed by the source endpoint [5].
- The encryption level must be 0rtt or 1rtt [6].
Effects:
(None) An endpoint that receives a STOP_SENDING frame MUST send a RESET_STREAM frame if the stream is in the Ready or Send state
object frame = { ...
object stop_sending = { ...
action handle(f:frame.stop_sending,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {# is_not_sleeping := time_api.c_timer.is_sleep_fake_timeout;
require (~is_not_sleeping -> ~_generating);
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid); # [6]
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
if _generating {
};
require ~conn_closed(scid); # [5]
require connected(scid) & connected_to(scid) = dcid;
if ~_generating { # For tests
require stream_seen(dcid,f.id); # [8]
require stream_id_allowed(dcid,f.id,e); # [4]
};
...
if ~_generating {
call handle_transport_error(f.err_code);
call handle_h3_error(f.err_code);
};
stream_seen(scid,f.id) := true;
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
max_streams event¤
max_streams frames cause the maximum stream id to be set. The receiver of the max stream id may use stream ids up to and including the given maximum. Bit 1 of the stream id (the next-to-least significant) determines whether the limit is set for unidirectional or bidirectional streams. A max stream id containing a stream id lower than the current maximum is allowed and ignored.
Requirements:
- The connection must not have been closed by the source endpoint [2].
- Max stream id frames may not occur in initial or handshake packets [3].
- The role of the stream id must equal the role of the peer in the given connection. [4] QUESTION: this requirement is not stated in the draft spec, but it is enforced by picoquic (see anomaly6). The spec should state explicitly what happens in this case. chris
- a lower stream limit than an endpoint has previously received. MAX_STREAMS frames that do not increase the stream limit MUST be ignored. [5] chris
Effects:
- The maximum stream id is set [1].
Question
must the stream id's be less than the max or less than or equal? Picoquic seems to think less than, but the is not clear in the draft.
var some_max_streams : bool; var ms;
object frame = { ...
object max_streams = { ...
action handle(f:frame.max_streams,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {# is_not_sleeping := time_api.c_timer.is_sleep_fake_timeout;
require (~is_not_sleeping -> ~_generating);
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid); # [3]
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require connected(scid) & connected_to(scid) = dcid;
if _generating {
};
require ~conn_closed(scid); # [2]
var kind := bidir;
if ~ (max_stream_set(dcid,kind) & f.id < max_stream(dcid,kind)) { #[5]
max_stream_set(dcid,kind) := true;
max_stream(dcid,kind) := f.id; # [1]
}
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
object frame = { ...
object max_streams_bidi = { ...
action handle(f:frame.max_streams_bidi,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {# is_not_sleeping := time_api.c_timer.is_sleep_fake_timeout;
require (~is_not_sleeping -> ~_generating);
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid); # [3]
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require connected(scid) & connected_to(scid) = dcid;
if _generating {
};
require ~conn_closed(scid); # [2]
var kind := bidir;
if ~ (max_stream_set(dcid,kind) & f.id < max_stream(dcid,kind)) { #[5]
max_stream_set(dcid,kind) := true;
max_stream(dcid,kind) := f.id; # [1]
}
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
CONNECT_CLOSE event¤
CONNECT_CLOSE frames indicate to the peer that the connection is being closed. It is unclear what this means operationally, but it seems reasonable to assume that the endpoint closing the connection will not send or receive any further data on the connection, so it is as if all the open streams are reset by this operation.
A connection close frame can occur at any time.
Questions:
- Are Ack frames still allowed after connection close?
- Are retransmissions allowed after connection close?
- When is a connection close allowed?
Requirements:
- The source and destination cid's must be connected. In effect, this means that a server hello message must have been sent for this connection Therefore a client cannot send a connection close before receiving at least one handshake message from the server. QUESTION: the spec is a bit vague about this, stating "Handshake packets MAY contain CONNECTION_CLOSE frames if the handshake is unsuccessful." Does "unsuccessful" necessarily mean that some handshake has been received? Also, can an initial packet contain connection close?
Effects:
- The connection state is set to closed for the source endpoint.
object frame = { ...
object connection_close = { ...
action handle(f:frame.connection_close,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle{
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.handshake -> established_handshake_keys(scid);
require e = quic_packet_type.one_rtt -> established_1rtt_keys(scid);
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
if _generating {
};
require connected(scid) & connected_to(scid) = dcid;
require f.reason_phrase_length = f.reason_phrase.end;
if _generating {
require e = quic_packet_type.one_rtt;
require ~conn_closed(scid);
}
else {
connection_closed := true;
};
conn_closed(scid) := true;
call handle_transport_error(f.err_code);
call handle_h3_error(f.err_code);
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
APPLICATION_CLOSE event¤
APPLICATION_CLOSE frames indicate to the peer that the connection is being closed. It is unclear what this means operationally, but it seems reasonable to assume that the endpoint closing the connection will not send or receive any further data on the connection, so it is as if all the open streams are reset by this operation. In the standard, an APPLICATION_CLOSE frame is described as CONNECTION_CLOSE frame with a special tag field. Here, we use a distinct variant type to represent it.
An application close frame can occur at any time.
Questions:
- Are ACK frames still allowed after application close?
- Are retransmissions allowed after application close?
- When is a application close allowed?
Requirements:
(None)
Effects:
- The connection state is set to closed for the source endpoint.
object frame = { ...
object application_close = { ...
action handle(f:frame.application_close,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle{
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
if _generating {
};
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require connected(scid) & connected_to(scid) = dcid;
require f.reason_phrase_length = f.reason_phrase.end;
conn_closed(scid) := true;
call handle_transport_error(f.err_code);
call handle_h3_error(f.err_code);
if ~_generating {
connection_closed := true;
};
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
MAX_STREAM_DATA event¤
MAX_STREAM_DATA frames set the limit on data bytes that the source endpoint is willing to receive for a given stream.
Requirements
- The stream must be open for receiving at the source endpoint [1]. (A MAX_STREAM_DATA frame can be sent for streams in the Recv state;) (Receiving a MAX_STREAM_DATA frame for a locally- initiated stream that has not yet been created MUST be treated as a connection error of type STREAM_STATE_ERROR)
Effects - If the given limit is greater than any previously set limit, then the max stream data limit for the given stream is updated [2].
object frame = { ...
object max_stream_data = { ...
action handle(f:frame.max_stream_data,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
if _generating {
};
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require stream_seen(scid,f.id);
if ~max_stream_data_set(scid,f.id) | f.pos > max_stream_data_val(scid,f.id) {
max_stream_data_set(scid,f.id) := true;
max_stream_data_val(scid,f.id) := f.pos; # [2]
}
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
stream_data_blocked event¤
| 0x15 | STREAM_DATA_BLOCKED | Section 19.13 | __01 |
stream_data_blocked frames indicate that sender wishes to send data on stream beyond current limit.
Requirements
- Connection must be established chris
- The stream must be open for receiving at the destination endpoint [1] An endpoint that receives a STREAM_DATA_BLOCKED frame for a send-only stream MUST terminate the connection with error STREAM_STATE_ERROR. chris Effects
(None)
object frame = { ...
object stream_data_blocked = { ...
action handle(f:frame.stream_data_blocked,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
if _generating {
};
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
data_blocked event¤
| 0x14 | DATA_BLOCKED | Section 19.12 | __01 |
data_blocked frames indicate that sender wishes to send data beyond current total limit for all streams.
Requirements
- Connection must be established
Effects
(None)
object frame = { ...
object data_blocked = { ...
action handle(f:frame.data_blocked,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
if _generating {
};
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
streams_blocked event¤
| 0x16 - 0x17 | STREAMS_BLOCKED | Section 19.14 | __01 |
streams_blocked frames indicate that sender wishes to open a stream beyond current limit on streams of a given kind.
Requirements
- Connection must be established chris A STREAMS_BLOCKED (by sender) frame of type 0x16 is used to indicate reaching the bidirectional stream limit, and a STREAMS_BLOCKED frame of type 0x17 is used to indicate reaching the unidirectional stream limit. => receiver should increase max_stream (TODO) chris Effects
(None)
object frame = { ...
object streams_blocked = { ...
action handle(f:frame.streams_blocked,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
if _generating {
};
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
object frame = { ...
object streams_blocked_bidi = { ...
action handle(f:frame.streams_blocked_bidi,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
if _generating {
};
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
MAX_DATA EVENT¤
| 0x10 | MAX_DATA | Section 19.9 | __01 |
MAX_DATA frames set the limit on the total data bytes that the source endpoint is willing to receive for all streams combined.
Requirements
(None)
Effects - If the given limit is greater than any previously set limit, then the max data limit for the connection is updated [2].
object frame = { ...
object max_data = { ...
action handle(f:frame.max_data,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
if _generating {
};
if ~max_data_set(scid) | f.pos > max_data_val(scid) {
max_data_set(scid) := true;
max_data_val(scid) := f.pos; # [2]
}
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
PING event¤
| 0x01 | PING | Section 19.2 | IH01 |
PING frames contain no data and have no semantics. They can be used to keep a connection alive.
object frame = { ...
object ping = { ...
action handle(f:frame.ping,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require e = quic_packet_type.handshake -> established_handshake_keys(scid);
require e = quic_packet_type.one_rtt -> established_1rtt_keys(scid);
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
if _generating {
require ~(e = quic_packet_type.version_negociation) & ~(e = quic_packet_type.retry) & ~(e = quic_packet_type.zero_rtt);
require need_sent_ack_eliciting_application_packet | need_sent_ack_eliciting_handshake_packet | need_sent_ack_eliciting_initial_packet;
};
...
if _generating {
need_sent_ack_eliciting_application_packet := false;
need_sent_ack_eliciting_handshake_packet := false;
need_sent_ack_eliciting_initial_packet := false;
}
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
unknown_frame event¤
unknown_frame frames contain no data and have no semantics. They can be used to keep a connection alive.
object frame = { ...
object unknown_frame = { ...
action handle(f:frame.unknown_frame,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
require ~conn_closed(scid);
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
PADDING event¤
PADDING frames contain no data and have no semantics. They can be used to keep a connection alive.
object frame = { ... object padding = { ... action handle(f:frame.padding,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num) after handle { call enqueue_frame(scid,f,e,true,seq_num); } } }
HANDSHAKE_DONE event¤
HANDSHAKE_DONE frames contain no data and have no semantics. They can be used to say handshake is done TODO
object frame = { ...
object handshake_done = { ...
action handle(f:frame.handshake_done,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid); # [3]
require e ~= quic_packet_type.initial;
require e ~= quic_packet_type.handshake;
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require tls_handshake_finished;
...
if _generating {
handshake_done_send := true;
}
else {
handshake_done_recv := true;
};
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
NEW_CONNECTION_ID event¤
NEW_CONNECTION_ID frames are used to transmit additional cid's to the peer. chris Requirements
- length field less than 1 and greater than 20 are invalid [1]
- An endpoint that is sending packets with a zero-length Destination Connection ID MUST treat receipt of a NEW_CONNECTION_ID frame as a connection error of type PROTOCOL_VIOLATION. [2]
- Receipt of the same frame multiple times MUST NOT be treated as a connection error. [3]
- The Retire Prior To field MUST be less than or equal to the Sequence Number field [4]
Effects
- A receiver MUST ignore any Retire Prior To fields that do not increase the largest received Retire Prior To value [5]
- An endpoint that receives a NEW_CONNECTION_ID frame with a sequence number smaller than the Retire Prior To field of a previously received NEW_CONNECTION_ID frame MUST send a corresponding RETIRE_CONNECTION_ID frame that retires the newly received connection ID, unless it has already done so for that sequence number. [6]
- An endpoint that selects a zero-length connection ID during the handshake cannot issue a new connection ID. [7]
chris
object frame = { ...
object new_connection_id = { ...
action handle(f:frame.new_connection_id,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
require num_queued_frames(scid) > 0 -> e = queued_level(scid); #Will change with implementing TODO
require ~issued_zero_length_cid; # [7]
if ~_generating { # For error test, carefull, should be specified in generating so
require f.retire_prior_to <= f.seq_num; #[4]
};
require f.seq_num < max_rtp_num(scid) -> send_retire_cid(dcid); #[6]
...
cid_mapped(f.scid) := true;
cid_to_aid(f.scid) := scid;
seqnum_to_cid(scid,f.seq_num) := f.scid;
last_cid_seq(scid) := f.seq_num; # ncid quant vuln
count_newcid_frame(f.seq_num,f.retire_prior_to,f.length,f.scid,f.token) := count_newcid_frame(f.seq_num,f.retire_prior_to,f.length,f.scid,f.token) + 1;
if count_newcid_frame(f.seq_num,f.retire_prior_to,f.length,f.scid,f.token) = 1 {
num_conn(dcid) := num_conn(dcid) + 1;
var tp := trans_params(dcid);
if ~_generating & active_connection_id_limit.is_set(tp) {
require acti_coid_check(dcid,num_conn(dcid));
};
};
if (f.retire_prior_to > max_rtp_num(scid)) {
max_rtp_num(scid) := f.retire_prior_to; #[5]
};
if (f.seq_num > max_seq_num(scid)) {
max_seq_num(scid) := f.seq_num;
};
call enqueue_frame(scid,f,e,true,seq_num);
}
}
}
RETIRE_CONNECTION_ID event¤
RETIRE_CONNECTION_ID frames are used to tell the sender of the new connection id that the connection id will no longer be used.
Requirements: - Receipt of a RETIRE_CONNECTION_ID frame containing a sequence number greater than any previously sent to the peer MUST be treated as a connection error of type PROTOCOL_VIOLATION. [1] - The sequence number specified in a RETIRE_CONNECTION_ID frame MUST NOT refer to the Destination Connection ID field of the packet in which the frame is contained. The peer MAY treat this as a connection error of type PROTOCOL_VIOLATION. [2] - An endpoint that is sending packets with a zero-length Destination Connection ID MUST treat receipt of a NEW_CONNECTION_ID frame as a connection error of type PROTOCOL_VIOLATION. [3] TODO
object frame = { ...
object retire_connection_id = { ...
action handle(f:frame.retire_connection_id,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require f.seq_num <= max_seq_num(dcid); #[1]
...
cid_mapped(seqnum_to_cid(dcid, f.seq_num)) := false; #[2]
count_rcid_frame(f.seq_num) := count_rcid_frame(f.seq_num) + 1;
if count_rcid_frame(f.seq_num) = 1 {
num_conn(dcid) := num_conn(dcid) - 1;
};
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
PATH_CHALLENGE event¤
Path challenge frames are used to request verification of ownership of an endpoint by a peer.
A pending path challenge value me not be retransmitted [1]. That is, according to quic-transport-draft-18, section 13.2:
PATH_CHALLENGE frames include a different payload each time they are sent.
Notice that we do allow a PATH_CHALLENGE payload to be re-used after it is responded to, on the theory that this is a new challenge and not a retransmission, however, it is unclear that this is the intention of the standard.
object frame = { ...
object path_challenge = { ...
action handle(f:frame.path_challenge,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
require handshake_done_recv | handshake_done_send;
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require f.data.end = 8;
require ~path_challenge_pending(dcid,f.data);
...
path_challenge_pending(dcid,f.data) := true;
call enqueue_frame(scid,f,e,true,seq_num);
}
}
}
PATH_RESPONSE event¤
PATH_RESPONSE frames are used to verify ownership of an endpoint in response to a path_challenge frame.
object frame = { ...
object path_response = { ...
action handle(f:frame.path_response,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
if _generating {
require ~path_challenge_sent(dcid); # avoid auto response
};
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require f.data.end = 8;
require path_challenge_pending(scid,f.data);
...
path_challenge_pending(scid,f.data) := false;
path_validated := true; # TODO
path_validated_pkt_num := seq_num;
call enqueue_frame(scid,f,e,true,seq_num);
}
}
}
NEW_TOKEN event¤
NEW_TOKEN frames are sent by the server to provide the client a token for establishing a new connection.
object frame = { ...
object new_token = { ...
action handle(f:frame.new_token,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require connected(dcid) & connected_to(dcid) = scid;
require e = quic_packet_type.one_rtt & established_1rtt_keys(scid);
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
if ~_generating {
require ~is_client(scid);
};
...
call tls_api.upper.save_token(f.data);
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
include quic_ack_frequency_extension
object frame = {
...
object malicious_frame = {
...
action handle(f:frame.malicious_frame,scid:cid,dcid:cid,e:quic_packet_type,seq_num:pkt_num)
around handle {
require tls_handshake_finished;
require connected(dcid) & connected_to(dcid) = scid;
require (e = quic_packet_type.one_rtt) & established_1rtt_keys(scid); # | e = quic_packet_type.zero_rtt | e = quic_packet_type.zero_rtt & established_0rtt_keys(scid)
require num_queued_frames(scid) > 0 -> e = queued_level(scid);
require ~conn_closed(scid); # [8]
require conn_seen(scid); # [9]
...
call enqueue_frame(scid,f,e,false,seq_num);
}
}
}
Frame events cause frames to be enqueued for transmission in a packet. This action enqueues a frame.
Effects:
- Appends frame to the frame queue for the given source endpoint and cid.
- Updates auxiliary functions
num_queued_framesandqueued_level.
Note: the auxilary functions contain redundant information that is useful for specifying packet events. By encoding history information in this way, we make it easier for constraint solvers to construct tests.
The argument probing indicates that the frame is a probing frame, according to [9.1] of the transport document( as of draft 23)
action enqueue_frame(scid:cid, f:frame, e:quic_packet_type, probing:bool, seq: pkt_num) = {
queued_frames(scid) := queued_frames(scid).append(f);
num_queued_frames(scid) := queued_frames(scid).end;
queued_level(scid) := e;
if ~probing {
queued_non_probing(scid) := true;
};
if ~(f isa frame.ack){ #& ~(f isa frame.padding){
queued_non_ack(scid) := true;
};
if f isa frame.path_challenge {
queued_challenge(scid) := true;
};
if (f isa frame.connection_close) | (f isa frame.application_close) {
queued_close(scid) := true;
};
if ~(f isa frame.ack) & ~(f isa frame.connection_close) { #& ~(f isa frame.padding){ & ~queued_ack_eliciting(scid)
queued_ack_eliciting(scid) := true;
if _generating {
queued_ack_eliciting_pkt(seqnum_to_streampos(last_pkt_num(scid,e) + 0x1)) := true; # TODO add client, vs server
};
}
}
action enqueue_frame_rtt(scid:cid, f:frame, e:quic_packet_type, probing:bool) = {
queued_frames_rtt(scid) := queued_frames_rtt(scid).append(f);
num_queued_frames_rtt(scid) := queued_frames_rtt(scid).end;
queued_level_rtt(scid) := e;
if ~(f isa frame.ack){ #& ~(f isa frame.padding){
queued_non_ack(scid) := true;
};
}
The maximum number of bytes that may be transmitted to a give aid on a given stream is computed by the following procedure. The number of bytes is the maximum of:
-
The receiver's
initial_max_stream_data_unitransport parameter, if the stream is unidirectional. -
The receiver's
initial_max_stream_data_bidi_localtransport parameter, if the stream is bidirectional and is initiated by the receiver. -
The receiver's
initial_max_stream_data_bidi_remotetransport parameter, if the stream is bidirectional and is initiated by the sender.
An alternative maximum lenght is given by the maximum total data limit for the receiving aid. That is, it can be no greater than the current stream length plus the maximum total additional bytes allowed on all streams.
An aid is the initiator of a stream if its protocol role (client or server) matches the role of the stream id.
TODO manage NCI
action stream_max_data(dcid:cid,id:stream_id, e:quic_packet_type) returns (max:stream_pos) = {
var tp := trans_params(dcid);
max := 0;
if get_stream_kind(id) = unidir {
if initial_max_stream_data_uni.is_set(tp) {
max := initial_max_stream_data_uni.value(trans_params(dcid)).stream_pos_32
}
} else {
if is_client(dcid) <-> get_stream_role(id) = role.client {
if initial_max_stream_data_bidi_local.is_set(tp) {
max := initial_max_stream_data_bidi_local.value(trans_params(dcid)).stream_pos_32
}
} else {
if initial_max_stream_data_bidi_remote.is_set(tp) {
max := initial_max_stream_data_bidi_remote.value(trans_params(dcid)).stream_pos_32
}
}
};
if max_stream_data_set(dcid,id) {
var msdv := max_stream_data_val(dcid,id);
max := msdv if msdv > max else max;
};
var alt_max := max_additional_data(dcid) + stream_length(dcid,id);
max := alt_max if alt_max < max else max;
if (zero_rtt_allowed & ~zero_rtt_sent) | (e = quic_packet_type.zero_rtt) { # TODO
max := 1000;
};
}
Whether a given stream can be opened by a peer of a given aid is computed by the following procedure. The id of a remotely initiated stream must be less than the maximum of:
-
Four times the aid's
initial_max_stream_id_unitransport parameter, if the stream is unidirectional [3]. -
Four times the aid's
initial_max_stream_id_biditransport parameter, if the stream is bidirectional [4]. -
The stream id parameter of any MAX_STREAM_ID frame sent by the aid, if it is of the same kind.
action stream_id_allowed(dcid:cid,id:stream_id,e: quic_packet_type) returns (ok:bool) = {
ok := false;
var tp := trans_params(dcid);
var kind := get_stream_kind(id);
var idhi : stream_id := id / 4;
if ~(is_client(dcid) <-> get_stream_role(id) = role.client) { # if stream remotely initiated
if kind = unidir {
if initial_max_stream_id_uni.is_set(tp) {
ok := idhi < (initial_max_stream_id_uni.value(tp).stream_id_16) # [3]
}
} else {
if initial_max_stream_id_bidi.is_set(tp) {
ok := idhi < (initial_max_stream_id_bidi.value(tp).stream_id_16); # [4]
}
};
ok := ok | max_stream_set(dcid,kind) & idhi < max_stream(dcid,kind);
}
else {
ok := stream_seen(dcid, id); # TODO: locally initiated streams must have been seen!
}
}
action stream_id_to_cid(bytes:stream_id) returns (val:cid) = {
<<<
val.val = 0;
for (unsigned i = 0; i < bytes.size(); i++)
val.val = (val.val << 8) + bytes[i];
>>>
}
action cid_to_stream_id(c:cid,len:cid_length) returns(res:stream_id) = {
<<<
res.resize(len);
for (unsigned i = 0; i < len; i++) {
res[len-i-1] = 0xff & (c.val >> (i * 8));
}
>>>
}
action cid_to_stream_pos(c:cid) returns(res:stream_pos) = {
<<<
res.resize(len);
for (unsigned i = 0; i < len; i++) {
res[len-i-1] = 0xff & (c.val >> (i * 8));
}
>>>
}
initial_max_data transport parameter
and the highest position sent by the aid in a max data frame. This is computed as the
maximum of these two values, less the total data already received.
action max_additional_data(dcid:cid) returns (max:stream_pos) = {
var tp := trans_params(dcid);
max := 0;
if initial_max_data.is_set(tp) {
max := initial_max_data.value(tp).stream_pos_32
};
if max_data_set(dcid) {
var smax := max_data_val(dcid);
max := smax if smax > max else max
};
max := max - conn_total_data(dcid); # note the substraction is saturating
}
action scale_ack_delay(delay:milliseconds, ack_delay_exponent:microsecs) returns (scaled:microseconds) = {
<<<
if (ack_delay_exponent == 0) {
ack_delay_exponent = 3;
}
std::cerr << "ack_delay_exponent " << ack_delay_exponent << "\n";
std::cerr << "delay " << delay << "\n";
std::cerr << "scaled " << delay * pow(ack_delay_exponent,2) << "\n";
scaled = delay * pow(ack_delay_exponent,2);
>>>
}
}
Check that the number of connection id proposed is not higher than active_connection_id_limit
action acti_coid_check(scid:cid,count:stream_pos) returns (ok:bool) = {
ok := true;
var max : stream_pos := 0;
var tp := trans_params(scid);
if active_connection_id_limit.is_set(tp) {
max := active_connection_id_limit.value(tp).stream_pos_32;
ok := count <= max;
};
}
import action show_ack_delay(t:microseconds)
import action show_pkt_num(p:pkt_num)
import action show_newly_acked(s:bool)
import action show_seqnum_to_streampos(p:stream_pos)
import action show_seqnum(p:pkt_num)