From 634444c547ea045846a438ec16d22dd7dc0adb5f Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 14 Sep 2018 17:34:43 -0700 Subject: [PATCH] working on picoquic.pcap --- doc/examples/quic/anomalies | 17 ++ doc/examples/quic/quic_connection.ivy | 321 +++++++++++++++++--------- doc/examples/quic/quic_deser.ivy | 89 ++++++- doc/examples/quic/quic_frame.ivy | 9 + doc/examples/quic/quic_infer.ivy | 23 +- doc/examples/quic/quic_types.ivy | 5 + doc/examples/quic/tls_protocol.ivy | 8 +- ivy/include/1.7/pcap.ivy | 44 ++-- 8 files changed, 369 insertions(+), 147 deletions(-) diff --git a/doc/examples/quic/anomalies b/doc/examples/quic/anomalies index c9f15d3..9ebc231 100644 --- a/doc/examples/quic/anomalies +++ b/doc/examples/quic/anomalies @@ -53,6 +53,23 @@ Issue: However, picoquic is putting these fields in the middle of the long header, before the length and the packet number fields. +Capture file: picoquic.pcap +Implementation: + picoquic +Endpoints: + - 10.0.0.1: server + - 10.0.0.2: client +Issue: + Packet 2 is an intial packet from the server to the client in repsonse + to Packet 1 fropm the cleint. It appears to have junk on the end. That + is, the payload length field appears to be correct, but there is additional + data after the end of the payload that appears to be garbage and might + be an information leak. + + On further inspection, the junk seems to be another QUIC packet. Somehow, + picoquic is cramming multiple QUIC packets into a single UDP packet. + + diff --git a/doc/examples/quic/quic_connection.ivy b/doc/examples/quic/quic_connection.ivy index b81afb2..5bef8d3 100644 --- a/doc/examples/quic/quic_connection.ivy +++ b/doc/examples/quic/quic_connection.ivy @@ -64,19 +64,19 @@ include quic_transport_parameters # server endpoint S is represented by `initial_pkt_cid(C,S)`. # TODO: unneeded as of version 11. should be removed # -# - For each endpoint E and cid C, last_pkt_num(E,C) represents the -# number of the latest packet sent by E on C. +# - For each endpoint E and cid C, last_pkt_num(E,C,L) represents the +# number of the latest packet sent by E on C in encryption level L. # -# - For each endpoint E and cid C, sent_pkt(E,C,N) is true if -# a packet numbered N has been sent by E on C. +# - For each endpoint E and cid C, sent_pkt(E,C,L,N) is true if +# a packet numbered N has been sent by E on C in encryption level L. # -# - For each endpoint E and cid C, acked_pkt(E,C,N) is true if -# a packet numbered N sent by E on connection C has been +# - For each endpoint E and cid C, acked_pkt(E,C,L,N) is true if +# a packet numbered N sent by E on connection C in encryption level L has been # acknowledged. # -# - For each endpoint E and cid C, max_acked(E,C) is the greatest -# packet number N such that acked_pkt(E,C,N), or zero if -# forall N. ~acked(E,C,N). +# - For each endpoint E and cid C, max_acked(E,C,L) is the greatest +# packet number N such that acked_pkt(E,C,L,N), or zero if +# forall N. ~acked(E,C,L,N). # # - For each endpoint E and cid C, ack_credit(E,C) is the number # of non-ack-only packets sent to E on C, less the number of @@ -86,6 +86,23 @@ include quic_transport_parameters # is true if endpoint E has declared transport parameters for # connection E. # +# - For each endpoint E, and destination cid C, `crypto_data(E,C,L)` +# represents the crypto data transmitted by TLS to endpoint E for +# cid C at encyption level L. This data may or may not have been +# transmitted in any QUIC packet. +# +# - For each endpoint E and destination cid C, `crypto_length(E,C,L)` +# indicates the length of the stream data transmitted in QUIC +# packets to endpoint E for cid C at encyption level L. 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 crypto +# data, but may not be greater. +# +# - For each endpoint E and destination cid C, `crypto_pos(E,C,L)` +# represents the read position of the crypto data transmitted by the application to endpoint E +# for cid C at encyption level L. This is the number of bytes in the stream that have +# been read by TLS at the destination. +# # - For each endpoint E, cid C,and stream id S, `stream_seen(E,C,S)` # indicates that a stream frame for stream id S on connection C # has been sent to destination endpoint E. @@ -137,21 +154,24 @@ include quic_transport_parameters # - The queued frames at source endpoint `E` for connection `C` are # represented by `queued_frames(E,C)` and are initially empty. # -# - The relation `queued_client_hello(E,C)` indicates that one of the queued -# frames at endpoint `E` for connection `C` contains a TLS client hello record. +# - The relation `queued_hello(E,C)` indicates that one of the queued +# frames at endpoint `E` for connection `C` contains a TLS hello record. # # - The function num_queued_frames(E:ip.endpoint,C:cid) gives the number of frames # queue at endpoint `E` for connection `C`. +# +# - The function `cid_dst_to_src(D,C)` maps the cid `C` at endpoint `D` to the +# corresponding cid of the per, if such a cid exists. relation conn_seen(E:ip.endpoint,C:cid) relation conn_closed(E:ip.endpoint,C:cid) relation initializing(C:ip.endpoint,S:ip.endpoint) function initial_pkt_num(C:ip.endpoint,S:ip.endpoint) : pkt_num function initial_pkt_cid(C:ip.endpoint,S:ip.endpoint) : cid -function last_pkt_num(E:ip.endpoint,C:cid) : pkt_num -relation sent_pkt(E:ip.endpoint,C:cid,N:pkt_num) -relation acked_pkt(E:ip.endpoint,C:cid,N:pkt_num) -function max_acked(E:ip.endpoint,C:cid) : pkt_num +function last_pkt_num(E:ip.endpoint,C:cid,L:encryption_level) : pkt_num +relation sent_pkt(E:ip.endpoint,C:cid,L:encryption_level,N:pkt_num) +relation acked_pkt(E:ip.endpoint,C:cid,L:encryption_level,N:pkt_num) +function max_acked(E:ip.endpoint,C:cid,L:encryption_level) : pkt_num function ack_credit(E:ip.endpoint,C:cid) : pkt_num relation trans_params_set(E:ip.endpoint,C:cid) function trans_params(E:ip.endpoint,C:cid) : trans_params_struct @@ -159,6 +179,11 @@ relation stream_seen(E:ip.endpoint,C:cid,S:stream_id) relation stream_open(E:ip.endpoint,C:cid,S:stream_id) function max_stream_data_val(E:ip.endpoint,C:cid,S:stream_id) : stream_pos relation max_stream_data_set(E:ip.endpoint,C:cid,S:stream_id) +function conn_enc_level(E:ip.endpoint,C:cid) : encryption_level +function crypto_data(E:ip.endpoint,C:cid,L:encryption_level) : stream_data +function crypto_data_end(E:ip.endpoint,C:cid,L:encryption_level) : stream_pos +function crypto_pos(E:ip.endpoint,C:cid,L:encryption_level) : stream_pos +function crypto_length(E:ip.endpoint,C:cid,L:encryption_level) : stream_pos function stream_app_data(E:ip.endpoint,C:cid,S:stream_id) : stream_data function stream_app_data_end(E:ip.endpoint,C:cid,S:stream_id) : stream_pos function stream_app_pos(E:ip.endpoint,C:cid,S:stream_id) : stream_pos @@ -168,12 +193,12 @@ relation stream_reset(E:ip.endpoint,C:cid,S:stream_id) relation max_stream_set(E:ip.endpoint,C:cid,K:stream_kind) function max_stream(E:ip.endpoint,C:cid,K:stream_kind) : stream_id function queued_frames(E:ip.endpoint,C:cid) : frame.arr -relation queued_client_hello(E:ip.endpoint,C:cid) +relation queued_hello(E:ip.endpoint,C:cid) function num_queued_frames(E:ip.endpoint,C:cid) : frame.idx relation cid_renamed(C:cid) relation cid_new_name(C:cid) function cid_orig_name(C:cid) : cid - +function cid_dst_to_src(D:ip.endpoint,C:cid) : cid @@ -187,9 +212,9 @@ function cid_orig_name(C:cid) : cid after init { conn_seen(E,C) := false; conn_closed(E,C) := false; - sent_pkt(E,C,N) := false; - acked_pkt(E,C,N) := false; - max_acked(E,C) := 0; + sent_pkt(E,C,L,N) := false; + acked_pkt(E,C,L,N) := false; + max_acked(E,C,L) := 0; ack_credit(E,C) := 0; trans_params_set(E:ip.endpoint,C:cid) := false; stream_seen(E,C,S) := false; @@ -198,9 +223,10 @@ after init { stream_finished(E,C,S) := false; stream_reset(E,C,S) := false; stream_app_pos(E,C,S) := 0; - queued_client_hello(E,C) := false; + queued_hello(E,C) := false; cid_renamed(C) := false; cid_new_name(C) := false; + conn_enc_level(E,C) := encryption_level.initial; } # Ghost events @@ -274,6 +300,14 @@ after app_send_event { } } +# Encryption level change + +action set_encryption_level(src:ip.endpoint, scid:cid, e:encryption_level) + +after set_encryption_level { + conn_enc_level(src,scid) := e; +} + # TLS send event # ============== # @@ -281,8 +315,8 @@ after app_send_event { # endpoint to its peer on a given connection. In concept it occurs at # the moment when the implmentation of TLS passes data to QUIC to be # transmitted to the peer. This is a ghost event, since it is not -# visible on the wire. However, it can easily be inferred by examine -# the QUIC steamm frames on stream id 0. +# visible on the wire. However, it can easily be inferred by examining +# the QUIC crypto frames. # # Requirements # @@ -291,7 +325,7 @@ after app_send_event { # # Effects # -# - The TLS data is appended to stream 0 [4]. +# - The TLS data is appended to the crypto data [4]. # # - The effect of each transmitted TLS record on the QUIC connection # state is defined by `handle_tls_record`, below [2]. A TLS @@ -301,19 +335,20 @@ after app_send_event { before tls_send_event(src:ip.endpoint, dst:ip.endpoint, scid:cid, dcid:cid, data : stream_data) { # require conn_open(src,dcid); # [3] - var tr := tls.parser.deserialize(data); # [1] - var idx := tr.begin; - while idx < tr.end { - var tls_rec := tr.value(idx); - call tls.event(src,dst,tls_rec); - call handle_tls_record(src,dst,scid,tls_rec); #[2] + var hs := tls.handshake_parser.deserialize(data); # [1] + var idx := hs.begin; + while idx < hs.end { + var h := hs.value(idx); + call tls.handshake_event(src,dst,h); + call handle_tls_handshake(src,dst,scid,h); #[2] idx := idx.next }; var jdx := data.begin; + var e := conn_enc_level(src,scid); while jdx < data.end { - stream_app_data(dst,dcid,0) := - stream_app_data(dst,dcid,0).append(data.value(jdx)); # [4] - stream_app_data_end(dst,dcid,0) := stream_app_data(dst,dcid,0).end; + crypto_data(dst,dcid,e) := + crypto_data(dst,dcid,e).append(data.value(jdx)); # [4] + crypto_data_end(dst,dcid,e) := crypto_data(dst,dcid,e).end; jdx := jdx.next } } @@ -325,17 +360,17 @@ before tls_send_event(src:ip.endpoint, dst:ip.endpoint, scid:cid, dcid:cid, data # This event corresponds to transfer of data from QUIC to the TLS # implementation. -action tls_recv_event(src:ip.endpoint, dst:ip.endpoint, dcid:cid, lo: stream_pos, hi : stream_pos) +action tls_recv_event(src:ip.endpoint, dst:ip.endpoint, dcid:cid, e : encryption_level, lo: stream_pos, hi : stream_pos) around tls_recv_event { - require lo < hi & lo = stream_app_pos(dst,dcid,0) & hi <= stream_length(dst,dcid,0); - # require (data.end) + stream_app_pos(dst,pcid,0) <= stream_length(dst,pcid,0); -# require 0 <= N & N < data.end -> data.value(N) = stream_app_data(dst,pcid,0).value(N + stream_app_pos(dst,pcid,0)); + require lo < hi & lo = crypto_pos(dst,dcid,e) & hi <= crypto_length(dst,dcid,e); + # require (data.end) + crypto_pos(dst,pcid,0) <= crypto_length(dst,pcid,0); +# require 0 <= N & N < data.end -> data.value(N) = crypto_data(dst,pcid,0).value(N + crypto_pos(dst,pcid,0)); ... - stream_app_pos(dst,dcid,0) := hi; - # stream_app_pos(dst,pcid,0) := stream_app_pos(dst,pcid,0) + data.end + crypto_pos(dst,dcid,e) := hi; + # crypto_pos(dst,pcid,0) := crypto_pos(dst,pcid,0) + data.end } @@ -404,21 +439,14 @@ action orig_cid(pcid:cid) returns(pcid:cid) = { # - The header type must be one of the above [8]. # # - An Initial packet represents an attempt by a client to establish a -# connection. The cid is arbitary, but must not have been previously -# seen. The initial packet must consist (apart from padding) of a -# single stream frame for stream zero, containing the initial security +# connection. The scid is arbitrary, but must not have been previously +# seen. The dcid is unspecified. The initial packet must consist (apart from padding) of a +# single crypto, containing the initial security # handshake information [1]. # # - A Handshake packet is sent in response to an Initial packet or -# a previous Handshake. In the latter case, the cid must match -# the original cid. -# -# - TEMPORARY: We require that only one connection be initializing for -# a given client endpoint at a given time [2]. This seems unreasonable, -# but otherwise there is no way to match Handshake packets to Initial -# packets, at least without looking at the security information. -# -# - A packet number may not be re-sent on a given connection. +# a previous Handshake. In the latter case, the dcid must match +# the scid provided by the peer. # # - Initial packets may not be sent on a cid that has # been closed by the sender [6]. @@ -426,23 +454,19 @@ action orig_cid(pcid:cid) returns(pcid:cid) = { # - Once a cid has been renamed by the server, it may no longer be used in a packet header. # Instead the new cid must be used. [9] # -# ### Effects +# - A sender may not re-use a packet number on a given scid [4]. # -# - The `conn_seen` and `sent_pkt` relations are updated to reflect -# the observed packet [1]. -# - The `last_pkt_num` functiona is updated to indicate the observed -# packets as most recent for the packet's source and cid. -# - For Initial packets, `initializing` is set to true for the packet's -# source and destination. The packet number is recorded in -# `initial_pkt_num` and the cid in `initial_pkt_cid` [3]. -# - For Handshake packets, `initializing` is set to false for the -# source and destination of the Initial packet (the reverse of the -# handshake packet). The initial packet is transfered to the cid -# - A sender may not re-use a packet number on a given cid [4]. # - A packet containing only ack frames and padding is *ack-only*. # For a given cid, the number of ack-only packets sent from src to dst # must not be greater than the number of non-ack-only packets sent # from dst to src [5]. + +# ### Effects +# +# - The `conn_seen` and `sent_pkt` relations are updated to reflect +# the observed packet [1]. +# - The `last_pkt_num` function is updated to indicate the observed +# packets as most recent for the packet's source and cid. # # # ### Notes @@ -466,31 +490,50 @@ around packet_event(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) { var dcid := pkt.dst_cid; var scid := pkt.hdr_cid; - # TEMPORARY: only support long packet format + # On long headers, both cids are given. Record the correspondence. - assert pkt.hdr_long; + if pkt.hdr_long { + cid_dst_to_src(dst,dcid) := scid + } + + # On short headers, the scid is not given, so we use the recorded value + + # TODO: this is not reliable for testing, since a short header might + # arrive before a corresping long header due to packet re-ordering. We + # need to handle this case. This is a general problem with the test setup: + # the specification applies to packets in the actual order of transmission, + # while the tester may receive them out-of-order. One fix for this would be + # to have the spec also allow re-ordering, but this might introduce some + # significant complexity. + + else { + scid := cid_dst_to_src(dst,dcid) + }; + + var e := conn_enc_level(src,scid); var pnum := decode_packet_number(src,dst,pkt); - require ~sent_pkt(src,scid,pnum); # [4] + require ~sent_pkt(src,scid,e,pnum); # [4] # The payload may not be empty require num_queued_frames(src,scid) > 0; # [7] - # A packet is in initial packet iff it contains a client hello. + # A packet is an initial packet iff it contains a client hello. - assert pkt.hdr_type = 0x7f <-> queued_client_hello(src,scid); + # TODO: what to say about this? + # assert pkt.hdr_type = 0x7f <-> queued_hello(src,scid); # Record that the connection has been seen from this source, and # the packet has been sent. conn_seen(src,scid) := true; # [1] - sent_pkt(src,scid,pnum) := true; # [1] + sent_pkt(src,scid,e,pnum) := true; # [1] # Record the packet number as latest seen - last_pkt_num(src,scid) := pnum; + last_pkt_num(src,scid,e) := pnum; # The payload must exactly match the queued frames. @@ -505,12 +548,18 @@ around packet_event(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) { ... + # TEMPORARY: The following are repeated because currently locals defined in + # the "before" section cannot be accessed in the "after" section. + var dcid := pkt.dst_cid; var scid := pkt.hdr_cid; + if ~pkt.hdr_long { + scid := cid_dst_to_src(dst,dcid) + }; if pkt.hdr_type = 0x7f { - require pkt.payload.end = 1; # [1] - require pkt.payload.value(0) isa frame.stream; + require forall (I:frame.idx) 0 <= I & I < pkt.payload.end -> + ((pkt.payload.value(I) isa frame.ack) | (pkt.payload.value(I) isa frame.crypto)); require ~conn_closed(src,scid); # [6] }; @@ -528,7 +577,7 @@ around packet_event(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) { # The queued frames are deleted queued_frames(src, scid) := frame.arr.empty; - queued_client_hello(src, scid) := false; + queued_hello(src, scid) := false; num_queued_frames(src, scid) := 0; } @@ -587,19 +636,20 @@ object frame = { action handle(f:frame.ack,src:ip.endpoint,dst:ip.endpoint,scid:cid,dcid:cid) around handle { + var e := conn_enc_level(src,scid); var idx : frame.ack.block.idx := 0; var last := f.largest_acked; - if max_acked(dst,dcid) < last { - max_acked(dst,dcid) := last; # [3] + if max_acked(dst,dcid,e) < last { + max_acked(dst,dcid,e) := last; # [3] }; while idx < f.ack_blocks.end { var ack_block := f.ack_blocks.value(idx); var upper := last - ack_block.gap; last := upper - ack_block.blocks; - require (last <= N & N <= upper) -> sent_pkt(dst,dcid,N); # [1] + require (last <= N & N <= upper) -> sent_pkt(dst,dcid,e,N); # [1] var jdx := last; while jdx <= upper { - acked_pkt(dst,dcid,jdx) := true; + acked_pkt(dst,dcid,e,jdx) := true; jdx := jdx + 1 }; # acked_pkt(dst,dcid,N) := (last <= N & N <= upper) | acked_pkt(dst,dcid,N); # [2] @@ -612,8 +662,7 @@ object frame = { } } -# Stream frames carry stream data. Stream id 0 is special, in that it -# carries only TLS handshake data in the form of TLS records. +# Stream frames carry stream data. # # Requirements: # @@ -624,15 +673,15 @@ object frame = { # - If the stream is finished, the the frame offset plus length must # not exceed the stream length [5]. # -# - Except on stream 0, the stream id must be less than or equal to +# - The stream id must be less than or equal to # the max stream id for the kind of the stream [6]. # -# - Except on stream 0, the stream must not have been reset [7]. +# - The stream must not have been reset [7]. # -# - The connection must not have bee closed by the source endpoint [8]. +# - The connection must not have been closed by the source endpoint [8]. # -# - For stream ids other than zero, the connection id must have been seen at the source [9] -# and the connection between source and destination must no be initializing [10]. +# - The connection id must have been seen at the source [9] +# and the connection between source and destination must not be initializing [10]. # Effects: # @@ -660,8 +709,9 @@ object frame = { require ~conn_closed(src,scid); # [8] - require ((f.offset) + (f.length)) <= stream_app_data_end(dst,dcid,f.id); - require f.data = stream_app_data(dst,dcid,f.id).segment(f.offset,f.offset+f.length); + var offset := f.offset if f.off else stream_length(dst,dcid,f.id); + require ((offset) + (f.length)) <= stream_app_data_end(dst,dcid,f.id); + require f.data = stream_app_data(dst,dcid,f.id).segment(offset,offset+f.length); var kind := get_stream_kind(f.id); require max_stream_set(dst,dcid,kind) -> f.id <= max_stream(dst,dcid,kind); # [6] @@ -686,9 +736,9 @@ object frame = { stream_length(dst,dcid,f.id) := 0; }; if max_stream_data_set(dst,dcid,f.id) { - require ((f.offset) + (f.length)) <= max_stream_data_val(dst,dcid,f.id) # [2] + require ((offset) + (f.length)) <= max_stream_data_val(dst,dcid,f.id) # [2] }; - var length := f.offset + f.length; + var length := offset + f.length; require stream_finished(dst,dcid,f.id) -> length <= stream_length(dst,dcid,f.id); # [5] if stream_length(dst,dcid,f.id) < length { stream_length(dst,dcid,f.id) := length @@ -705,6 +755,43 @@ object frame = { } } +# Crypto frames carry crypto handshake data, that is, TLS records. +# +# Requirements: +# +# - The connection must not have bee closed by the source endpoint [1]. +# +# Effects: +# +# - The length of the crypto stream is updated. +# + +object frame = { + ... + object crypto = { + ... + action handle(f:frame.crypto,src:ip.endpoint,dst:ip.endpoint,scid:cid,dcid:cid) + + around handle { + + var e := conn_enc_level(src,scid); + call show_enc_level(e); + require ~conn_closed(src,scid); # [1] + + require ((f.offset) + (f.length)) <= crypto_data_end(dst,dcid,e); + require f.data = crypto_data(dst,dcid,e).segment(f.offset,f.offset+f.length); + + var length := f.offset + f.length; + if crypto_length(dst,dcid,e) < length { + crypto_length(dst,dcid,e) := length + }; + ... + queued_frames(src,scid) := queued_frames(src,scid).append(f); + num_queued_frames(src, scid) := queued_frames(src,scid).end; + } + } +} + # 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. @@ -841,6 +928,20 @@ object frame = { ... } } +# 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,src:ip.endpoint,dst:ip.endpoint,scid:cid,dcid:cid) + after handle { + queued_frames(src,scid) := queued_frames(src,scid).append(f); + num_queued_frames(src, scid) := queued_frames(src,scid).end; + } + } +} + + # ### Packet number decoding # The packet number is decoded from the packet header fields as follows. @@ -895,7 +996,13 @@ object frame = { ... action decode_packet_number(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) returns (pnum:pkt_num) = { var scid := pkt.hdr_cid; - var la := max_acked(src,scid); + + if ~pkt.hdr_long { + scid := cid_dst_to_src(dst,pkt.dst_cid) + }; + + var e := conn_enc_level(src,scid); + var la := max_acked(src,scid,e); pnum := pkt.hdr_pkt_num; @@ -903,7 +1010,7 @@ action decode_packet_number(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) ret # This is a last number transmitted by the source on this connection. - var last := last_pkt_num(src,scid); + var last := last_pkt_num(src,scid,e); # If long format or type is 0x1d, we match 32 bits @@ -940,27 +1047,21 @@ action decode_packet_number(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) ret # the reference `quic_transport_parameters`. Here we define the # protocol rules associated with `quic_transport_parameters`. # -# The `handle_tls_extensions` rules apply to each `client_hello` or -# `server_hello` message, in order of occurrence in a handshake -# record. The last parameter, `is_client_hello`, is true for a `client_hello` +# The `handle_tls_handshake` rules apply to each `client_hello` or +# `server_hello` message, in order of occurrence in the crypto data. +# The last parameter, `is_client_hello`, is true for a `client_hello` # message (see below). -action handle_tls_record(src:ip.endpoint,dst:ip.endpoint,scid:cid,tls_rec:tls.record) = { +action handle_tls_handshake(src:ip.endpoint,dst:ip.endpoint,scid:cid,hs:tls.handshake) = { - if some(hr:tls.handshake_record) tls_rec *> hr { - var idx := hr.fragment.begin; - while idx < hr.fragment.end { - var hs := hr.fragment.value(idx); - if some(ch:tls.client_hello) hs *> ch { - queued_client_hello(src,scid) := true; - call handle_tls_extensions(src,dst,scid,ch.extensions,true); - }; - if some(sh:tls.server_hello) hs *> sh { - call handle_tls_extensions(src,dst,scid,sh.extensions,false); - }; - idx := idx.next - } - } + if some(ch:tls.client_hello) hs *> ch { + queued_hello(src,scid) := true; + call handle_tls_extensions(src,dst,scid,ch.extensions,true); + }; + if some(sh:tls.server_hello) hs *> sh { + queued_hello(src,scid) := true; + call handle_tls_extensions(src,dst,scid,sh.extensions,false); + }; } # Requirements: @@ -1049,3 +1150,7 @@ action client_transport_parameters_event(src:ip.endpoint,dst:ip.endpoint,scid:ci tps:quic_transport_parameters) import client_transport_parameters_event + +action show_enc_level(e:encryption_level) + +import show_enc_level diff --git a/doc/examples/quic/quic_deser.ivy b/doc/examples/quic/quic_deser.ivy index 5c1bf66..2fe4cc8 100644 --- a/doc/examples/quic/quic_deser.ivy +++ b/doc/examples/quic/quic_deser.ivy @@ -32,6 +32,9 @@ object quic_deser = {} quic_stream_offset, quic_stream_length, quic_stream_data, + quic_crypto_offset, + quic_crypto_length, + quic_crypto_data, quic_ack_largest, quic_ack_delay, quic_ack_block_count, @@ -41,6 +44,7 @@ object quic_deser = {} quic_reset_err_code, quic_reset_final_offset, quic_connection_close_err_code, + quic_connection_close_frame_type, quic_connection_close_reason_length, quic_connection_close_reason, quic_max_stream_data_id, @@ -53,10 +57,13 @@ object quic_deser = {} int data_remaining; long long ack_blocks_expected; long long ack_block_count; - + int payload_length; + int fence; + public: quic_deser(const std::vector &inp) : ivy_binary_deser(inp),state(quic_s_init) { // pos = 42; // skip 42 bytes of IP and UDP header + fence = 0; } virtual void get(long long &res) { switch (state) { @@ -86,10 +93,15 @@ object quic_deser = {} break; case quic_s_dcil: { - getn(res,1); - scil = res & 0xf; - dcil = (res & 0xf0) >> 4; - res = dcil; + if (long_format) { + getn(res,1); + scil = res & 0xf; + dcil = (res & 0xf0) >> 4; + } else { + dcil = 5; + scil = 0; // TODO: how to determine the cid length? + } + res = dcil; state = quic_s_scil; } break; @@ -113,13 +125,24 @@ object quic_deser = {} break; case quic_s_payload_length: { - get_var_int(res); + if (long_format) { + get_var_int(res); + } else { + res = 0; + } + payload_length = res; state = quic_s_pkt_num; } break; case quic_s_pkt_num: { - ivy_binary_deser::getn(res,(long_format || (hdr_type & 0x1f) == 0x1d) ? 4 : (hdr_type & 0x1f) == 0x1e ? 2 : 1); + fence = 0; + if (payload_length > 0) { + fence = pos + payload_length - 16; + } else { + fence = inp.size() - 16; + } + get_pkt_num(res); state = quic_s_payload; } break; @@ -164,7 +187,21 @@ object quic_deser = {} state = quic_stream_data; } break; + case quic_crypto_offset: + { + get_var_int(res); + state = quic_crypto_length; + } + break; + case quic_crypto_length: + { + get_var_int(res); + data_remaining = res; + state = quic_crypto_data; + } + break; case quic_stream_data: + case quic_crypto_data: case quic_connection_close_reason: case quic_s_retry_token: { @@ -219,6 +256,12 @@ object quic_deser = {} case quic_connection_close_err_code: { getn(res,2); + state = quic_connection_close_frame_type; + } + break; + case quic_connection_close_frame_type: + { + get_var_int(res); state = quic_connection_close_reason_length; } break; @@ -258,6 +301,19 @@ object quic_deser = {} res |= (lobyte & 0x3f) << (bytes << 3); } + void get_pkt_num(long long &res) { + static int lens[4] = {0,0,1,3}; + long long lobyte; + ivy_binary_deser::getn(lobyte,1); + int bytes = lens[(lobyte & 0xc0) >> 6]; + if (bytes == 0) { + res = lobyte; + return; + } + ivy_binary_deser::getn(res,bytes); + res |= (lobyte & 0x3f) << (bytes << 3); + } + virtual int open_tag(const std::vector &tags) { if (state == quic_s_payload) { long long ft; @@ -267,7 +323,7 @@ object quic_deser = {} state = quic_stream_off; return 0; } - if (frame_type == 0x0e) { + if (frame_type == 0x0d) { state = quic_ack_largest; return 1; } @@ -291,6 +347,13 @@ object quic_deser = {} state = quic_reset_final_offset; return 6; } + if (frame_type == 0x18) { + state = quic_crypto_offset; + return 7; + } + if (frame_type == 0x07) { + return 8; + } std::cerr << "saw tag " << ft << std::endl; } throw deser_err(); @@ -298,9 +361,9 @@ object quic_deser = {} virtual bool open_list_elem() { if (state == quic_s_payload) { - while (more(1) && inp[pos] == 0) + while ((fence == 0 || pos < fence) && more(1) && inp[pos] == 0) pos++; // skip padding frames - return more(1); + return (fence == 0 || pos < fence) && more(1); } if (state == quic_ack_gap) { return ack_block_count < ack_blocks_expected; @@ -311,6 +374,8 @@ object quic_deser = {} return data_remaining-- > 0; if (state == quic_s_retry_token) return data_remaining-- > 0; + if (state == quic_crypto_data) + return data_remaining-- > 0; throw deser_err(); } @@ -323,6 +388,10 @@ object quic_deser = {} } } void close_list() { + if (state == quic_s_payload) { + state = quic_s_init; + pos += 16; // skip the checksum + } if (state == quic_s_retry_token) { state = quic_s_payload_length; } diff --git a/doc/examples/quic/quic_frame.ivy b/doc/examples/quic/quic_frame.ivy index 15310a0..31aa5e1 100644 --- a/doc/examples/quic/quic_frame.ivy +++ b/doc/examples/quic/quic_frame.ivy @@ -81,6 +81,7 @@ object frame = { 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 } @@ -117,6 +118,14 @@ object frame = { } } + object ping = { + + # Ping frames contain no data + + variant this of frame = struct { + } + } + instance idx : unbounded_sequence instance arr : array(idx,this) } diff --git a/doc/examples/quic/quic_infer.ivy b/doc/examples/quic/quic_infer.ivy index 5b78815..bddc610 100644 --- a/doc/examples/quic/quic_infer.ivy +++ b/doc/examples/quic/quic_infer.ivy @@ -4,7 +4,7 @@ # Ghost event inference # --------------------- # -# As an aid in monitoring UIC packet streams, this section provides +# As an aid in monitoring QUIC packet streams, this section provides # actions for inferring unobserved ghost events from QUIC packet # events. @@ -23,16 +23,31 @@ action infer_tls_events(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet) = { var scid := pkt.hdr_cid; var dcid := pkt.dst_cid; + + # On short headers, the scid is not given, so we use the recorded value + + if ~pkt.hdr_long { + scid := cid_dst_to_src(dst,dcid) + }; + + # the encryption level of frames has to be inferred from the packet header + + var e := encryption_level.initial if (pkt.hdr_type = 0x7f) + else (encryption_level.handshake if pkt.hdr_type = 0x7d + else encryption_level.other); + + call set_encryption_level(src,scid,e); # if initializing(dst,src) { [1] # call rename_connection(src,dst,initial_pkt_cid(dst,src),pcid) # }; var idx := pkt.payload.begin; while idx < pkt.payload.end { var f := pkt.payload.value(idx); + if some(cf:frame.crypto) f *> cf { + call tls_send_event(src,dst,scid,dcid,cf.data) + }; if some(sf:frame.stream) f *> sf { - if sf.id = 0 { - call tls_send_event(src,dst,scid,dcid,sf.data) - } + call app_send_event(src,dst,dcid,sf.id,sf.data) }; call show_frame(src,dst,scid,dcid,f); call f.handle(src,dst,scid,dcid); diff --git a/doc/examples/quic/quic_types.ivy b/doc/examples/quic/quic_types.ivy index 8e225b6..b2b3065 100644 --- a/doc/examples/quic/quic_types.ivy +++ b/doc/examples/quic/quic_types.ivy @@ -73,3 +73,8 @@ object role = { type this = {client,server} } +# encryption levels + +object encryption_level = { + type this = {initial,handshake,other} +} diff --git a/doc/examples/quic/tls_protocol.ivy b/doc/examples/quic/tls_protocol.ivy index 4dfced7..c9056e5 100644 --- a/doc/examples/quic/tls_protocol.ivy +++ b/doc/examples/quic/tls_protocol.ivy @@ -22,18 +22,18 @@ object tls = { ... # Record parser # ============= - instance records : vector(record) - instance parser : deserializer(stream_data,records,tls_deser) + instance handshakes : vector(handshake) + instance handshake_parser : deserializer(stream_data,handshakes,tls_deser) # Protocol event # ============== - action event(src : ip.endpoint, dst : ip.endpoint, rec : tls.record) + action handshake_event(src : ip.endpoint, dst : ip.endpoint, h : handshake) } # For the moment, we don't monitor TLS, just output the records. -import tls.event +import tls.handshake_event diff --git a/ivy/include/1.7/pcap.ivy b/ivy/include/1.7/pcap.ivy index bf43e98..aec9be1 100644 --- a/ivy/include/1.7/pcap.ivy +++ b/ivy/include/1.7/pcap.ivy @@ -139,30 +139,32 @@ module pcap(pkt,deser) = { // Create a deserializer and deserialize the packet. deser ds(buf); - pkt packet; - try { - __deser(ds,packet); - } - - // If deserialization failure, print out the packet for - // debugging purposes. - - catch(deser_err &err) { - std::cerr << "error: failed to deserialize packet in pcap file." << std::endl; - std::cerr << "hex dump of packet follows." << std::endl; - for (unsigned i = 0; i < buf.size(); i++) { - if (i > 0 && i % 16 == 0) - std::cerr << std::endl; - if (i == ds.pos) - fprintf(stderr,"*"); - fprintf(stderr,"%02X",((unsigned)buf[i]) & 0xff); + while (ds.inp.size() > ds.pos) { + pkt packet; + try { + __deser(ds,packet); } + + // If deserialization failure, print out the packet for + // debugging purposes. + + catch(deser_err &err) { + std::cerr << "error: failed to deserialize packet in pcap file." << std::endl; + std::cerr << "hex dump of packet follows." << std::endl; + for (unsigned i = 0; i < buf.size(); i++) { + if (i > 0 && i % 16 == 0) + std::cerr << std::endl; + if (i == ds.pos) + fprintf(stderr,"*"); + fprintf(stderr,"%02X",((unsigned)buf[i]) & 0xff); + } + } + + // Finally, if we got a good packet, hit the callback. + + cb(src,dst,packet); } - - // Finally, if we got a good packet, hit the callback. - - cb(src,dst,packet); } };