Commit 098b83ba authored by Paul's avatar Paul
Browse files

verify tcp_input.c

parent ebc50b26
From refinedc.typing Require Import typing.
Record tcp_ecn_flags := mk_tcp_ecn_flags {
ecn_ok : bool;
ecn_queue_cwr : bool;
ecn_demand_cwr : bool;
ecn_seen : bool;
}.
Global Instance tcp_ecn_flags_settable : Settable _ := settable! mk_tcp_ecn_flags
<ecn_ok; ecn_queue_cwr; ecn_demand_cwr; ecn_seen>.
Definition tcp_ecn_flags_repr (f : tcp_ecn_flags) : Z :=
bf_cons 0 1 (Z_of_bool $ ecn_ok f) $
bf_cons 1 1 (Z_of_bool $ ecn_queue_cwr f) $
bf_cons 2 1 (Z_of_bool $ ecn_demand_cwr f) $
bf_cons 3 1 (Z_of_bool $ ecn_seen f) $
bf_nil.
Arguments tcp_ecn_flags_repr _/.
Definition tcp_ecn_flags_wf (f : tcp_ecn_flags) : Prop :=
0 Z_of_bool $ ecn_ok f < 2^1
0 Z_of_bool $ ecn_queue_cwr f < 2^1
0 Z_of_bool $ ecn_demand_cwr f < 2^1
0 Z_of_bool $ ecn_seen f < 2^1.
Global Instance tcp_ecn_flags_BitFieldDesc : BitfieldDesc tcp_ecn_flags := {|
bitfield_it := u8;
bitfield_repr := tcp_ecn_flags_repr;
bitfield_wf := tcp_ecn_flags_wf;
|}.
Global Instance simpl_exist_tcp_ecn_flags P : SimplExist tcp_ecn_flags P
( ok queue_cwr demand_cwr seen,
P {|
ecn_ok := ok;
ecn_queue_cwr := queue_cwr;
ecn_demand_cwr := demand_cwr;
ecn_seen := seen;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_tcp_ecn_flags P : SimplForall tcp_ecn_flags 4 P
( ok queue_cwr demand_cwr seen,
P {|
ecn_ok := ok;
ecn_queue_cwr := queue_cwr;
ecn_demand_cwr := demand_cwr;
ecn_seen := seen;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record inet_csk_ack_state := mk_inet_csk_ack_state {
ack_sched : bool;
ack_timer : bool;
ack_pushed : bool;
ack_pushed_2 : bool;
ack_now : bool;
}.
Global Instance inet_csk_ack_state_settable : Settable _ := settable! mk_inet_csk_ack_state
<ack_sched; ack_timer; ack_pushed; ack_pushed_2; ack_now>.
Definition inet_csk_ack_state_repr (f : inet_csk_ack_state) : Z :=
bf_cons 0 1 (Z_of_bool $ ack_sched f) $
bf_cons 1 1 (Z_of_bool $ ack_timer f) $
bf_cons 2 1 (Z_of_bool $ ack_pushed f) $
bf_cons 3 1 (Z_of_bool $ ack_pushed_2 f) $
bf_cons 4 1 (Z_of_bool $ ack_now f) $
bf_nil.
Arguments inet_csk_ack_state_repr _/.
Definition inet_csk_ack_state_wf (f : inet_csk_ack_state) : Prop :=
0 Z_of_bool $ ack_sched f < 2^1
0 Z_of_bool $ ack_timer f < 2^1
0 Z_of_bool $ ack_pushed f < 2^1
0 Z_of_bool $ ack_pushed_2 f < 2^1
0 Z_of_bool $ ack_now f < 2^1.
Global Instance inet_csk_ack_state_BitFieldDesc : BitfieldDesc inet_csk_ack_state := {|
bitfield_it := u8;
bitfield_repr := inet_csk_ack_state_repr;
bitfield_wf := inet_csk_ack_state_wf;
|}.
Global Instance simpl_exist_inet_csk_ack_state P : SimplExist inet_csk_ack_state P
( sched timer pushed pushed_2 now,
P {|
ack_sched := sched;
ack_timer := timer;
ack_pushed := pushed;
ack_pushed_2 := pushed_2;
ack_now := now;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_inet_csk_ack_state P : SimplForall inet_csk_ack_state 5 P
( sched timer pushed pushed_2 now,
P {|
ack_sched := sched;
ack_timer := timer;
ack_pushed := pushed;
ack_pushed_2 := pushed_2;
ack_now := now;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record inet_csk_ack := {
ack_pending : inet_csk_ack_state;
}.
Global Instance simpl_exist_inet_csk_ack P : SimplExist inet_csk_ack P
( pending, P {| ack_pending := pending; |}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_inet_csk_ack P : SimplForall inet_csk_ack 1 P
( pending, P {| ack_pending := pending; |}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record tcp_header := {
tcp_cwr : bool;
tcp_ece : bool;
tcp_syn : bool;
}.
Global Instance simpl_exist_tcp_header P : SimplExist tcp_header P
( cwr ece syn,
P {|
tcp_cwr := cwr;
tcp_ece := ece;
tcp_syn := syn;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_tcp_header P : SimplForall tcp_header 3 P
( cwr ece syn,
P {|
tcp_cwr := cwr;
tcp_ece := ece;
tcp_syn := syn;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record tcp_skb_control := {
tcp_seq : Z;
tcp_end_seq : Z;
}.
//@rc::import tcp_input_lemmas from refinedc.linux.casestudies.tcp_input
#include <stdbool.h>
#include "bits.h"
// include/net/sock.h
struct sock {
// we don't care the actual fields of this struct
int dummy;
};
// include/linux/skbuff.h
struct sk_buff {
// we don't care the actual fields of this struct
int dummy;
};
// include/uapi/linux/tcp.h
struct tcphdr {
struct [[rc::refined_by("hdr : tcp_header")]] tcphdr {
[[rc::field("{tcp_cwr hdr} @ boolean<bool_it>")]]
bool cwr;
[[rc::field("{tcp_ece hdr} @ boolean<bool_it>")]]
bool ece;
[[rc::field("{tcp_syn hdr} @ boolean<bool_it>")]]
bool syn;
};
// include/linux/tcp.h
struct tcp_sock {
struct [[rc::refined_by("flags : tcp_ecn_flags")]] tcp_sock {
[[rc::field("flags @ bitfield<tcp_ecn_flags>")]]
u8 ecn_flags; /* ECN status bits. */
};
static inline struct tcp_sock *tcp_sk(const struct sock *sk);
static inline struct tcphdr *tcp_hdr(const struct sk_buff *skb);
// include/net/tcp.h
#define TCP_ECN_OK BIT(0)
#define TCP_ECN_QUEUE_CWR BIT(1)
#define TCP_ECN_DEMAND_CWR BIT(2)
#define TCP_ECN_SEEN BIT(3)
#define TCP_ECN_OK BIT(0)
#define TCP_ECN_QUEUE_CWR BIT(1)
#define TCP_ECN_DEMAND_CWR BIT(2)
#define TCP_ECN_SEEN BIT(3)
/* This is what the send packet queuing engine uses to pass
* TCP per-packet control information to the transmission code.
......@@ -43,60 +32,92 @@ static inline struct tcphdr *tcp_hdr(const struct sk_buff *skb);
* This is 44 bytes if IPV6 is enabled.
* If this grows please adjust skbuff.h:skbuff->cb[xxx] size appropriately.
*/
struct tcp_skb_cb {
u32 seq; /* Starting sequence number */
struct [[rc::refined_by("cb : tcp_skb_control")]] tcp_skb_cb {
[[rc::field("{tcp_seq cb} @ int<u32>")]]
u32 seq; /* Starting sequence number */
[[rc::field("{tcp_end_seq cb} @ int<u32>")]]
u32 end_seq; /* SEQ + FIN + SYN + datalen */
u8 ip_dsfield; /* IPv4 tos or IPv6 dsfield */
};
static inline struct tcp_skb_cb *TCP_SKB_CB(const struct sk_buff *skb);
// include/net/inet_connection_sock.h
/** inet_connection_sock - INET connection oriented sock
* @icsk_ack: Delayed ACK control data
*/
struct inet_connection_sock {
struct {
u8 pending; /* ACK is pending */
// __u8 quick; /* Scheduled number of quick acks */
// __u8 pingpong; /* The session is interactive */
// __u8 retry; /* Number of attempts */
// __u32 ato; /* Predicted tick of soft clock */
// unsigned long timeout; /* Currently scheduled timeout */
// __u32 lrcvtime; /* timestamp of last received data packet */
// __u16 last_seg_size; /* Size of last incoming segment */
// __u16 rcv_mss; /* MSS used for delayed ACK decisions */
} icsk_ack;
*/
struct [[rc::refined_by("ack : inet_csk_ack")]] icsk_ack_t {
[[rc::field("{ack_pending ack} @ bitfield<inet_csk_ack_state>")]]
u8 pending; /* ACK is pending */
// __u8 quick; /* Scheduled number of quick acks */
// __u8 pingpong; /* The session is interactive */
// __u8 retry; /* Number of attempts */
// __u32 ato; /* Predicted tick of soft clock */
// unsigned long timeout; /* Currently scheduled timeout */
// __u32 lrcvtime; /* timestamp of last received data packet */
// __u16 last_seg_size; /* Size of last incoming segment */
// __u16 rcv_mss; /* MSS used for delayed ACK decisions */
} icsk_ack;
struct [[rc::refined_by("ack : inet_csk_ack")]] inet_connection_sock {
[[rc::field("ack @ icsk_ack_t")]]
struct icsk_ack_t icsk_ack;
};
static inline struct inet_connection_sock *inet_csk(const struct sock *sk);
// In the original program, there is struct pointer case between
// sock <-> tcp_sock, inet_csk
// sk_buff <-> tcphdr, tcp_skb_cb
// For now, simplify the definiton of sock and sk_buff to directly contain the struct they can cast
// include/net/inet_ecn.h
enum {
INET_ECN_NOT_ECT = 0,
INET_ECN_ECT_1 = 1,
INET_ECN_ECT_0 = 2,
INET_ECN_CE = 3,
INET_ECN_MASK = 3,
struct [[rc::refined_by("flags : tcp_ecn_flags", "ack : inet_csk_ack")]] sock
{
[[rc::field("&own<flags @ tcp_sock>")]]
struct tcp_sock* tcp_sk;
[[rc::field("&own<ack @ inet_connection_sock>")]]
struct inet_connection_sock* inet_csk;
};
enum inet_csk_ack_state_t {
ICSK_ACK_SCHED = 1,
ICSK_ACK_TIMER = 2,
ICSK_ACK_PUSHED = 4,
ICSK_ACK_PUSHED2 = 8,
ICSK_ACK_NOW = 16 /* Send the next ACK immediately (once) */
#define tcp_sk(sk) ((sk)->tcp_sk)
#define inet_csk(sk) ((sk)->inet_csk)
struct [[rc::refined_by("hdr : tcp_header", "cb : tcp_skb_control")]] sk_buff
{
[[rc::field("&own<hdr @ tcphdr>")]]
struct tcphdr* hdr;
[[rc::field("&own<cb @ tcp_skb_cb>")]]
struct tcp_skb_cb* cb;
};
#define tcp_hdr(skb) ((skb)->hdr)
#define TCP_SKB_CB(skb) ((skb)->cb)
// include/net/inet_ecn.h
// enum inet_csk_ack_state_t
#define ICSK_ACK_SCHED BIT(0)
#define ICSK_ACK_TIMER BIT(1)
#define ICSK_ACK_PUSHED BIT(2)
#define ICSK_ACK_PUSHED2 BIT(3)
#define ICSK_ACK_NOW BIT(4) /* Send the next ACK immediately (once) */
// tcp_input functions for tcp ecn
[[rc::parameters("flags : tcp_ecn_flags", "p : loc")]]
[[rc::args("p @ &own<flags @ tcp_sock>")]]
[[rc::requires("{bitfield_wf flags}")]]
[[rc::ensures("own p : {flags <| ecn_queue_cwr := (ecn_ok flags) || (ecn_queue_cwr flags) |>} @ tcp_sock")]]
static void tcp_ecn_queue_cwr(struct tcp_sock *tp)
{
if (tp->ecn_flags & TCP_ECN_OK)
tp->ecn_flags |= TCP_ECN_QUEUE_CWR;
}
[[rc::parameters("flags : tcp_ecn_flags", "ack : inet_csk_ack", "psk : loc",
"hdr : tcp_header", "cb : tcp_skb_control", "pskb : loc", "b : bool")]]
[[rc::args("psk @ &own<{(flags, ack)} @ sock>", "pskb @ &own<{(hdr, cb)} @ sk_buff>")]]
[[rc::requires("{bitfield_wf flags}")]]
[[rc::requires("{bitfield_wf (ack_pending ack)}")]]
[[rc::requires("{b = (tcp_cwr hdr) && bool_decide (tcp_seq cb ≠ tcp_end_seq cb)}")]]
[[rc::ensures("own psk : {(flags <| ecn_demand_cwr := negb (tcp_cwr hdr) && (ecn_demand_cwr flags) |>, "
"{| ack_pending := (ack_pending ack) <| ack_now := b || (ack_now (ack_pending ack)) |> |})} @ sock")]]
[[rc::ensures("own pskb : {(hdr, cb)} @ sk_buff")]]
static void tcp_ecn_accept_cwr(struct sock *sk, const struct sk_buff *skb)
{
if (tcp_hdr(skb)->cwr) {
......@@ -111,62 +132,45 @@ static void tcp_ecn_accept_cwr(struct sock *sk, const struct sk_buff *skb)
}
}
[[rc::parameters("flags : tcp_ecn_flags", "p : loc")]]
[[rc::args("p @ &own<flags @ tcp_sock>")]]
[[rc::requires("{bitfield_wf flags}")]]
[[rc::ensures("own p : {flags <| ecn_queue_cwr := false |>} @ tcp_sock")]]
static void tcp_ecn_withdraw_cwr(struct tcp_sock *tp)
{
tp->ecn_flags &= ~TCP_ECN_QUEUE_CWR;
}
static void __tcp_ecn_check_ce(struct sock *sk, const struct sk_buff *skb)
{
struct tcp_sock *tp = tcp_sk(sk);
switch (TCP_SKB_CB(skb)->ip_dsfield & INET_ECN_MASK) {
case INET_ECN_NOT_ECT:
/* Funny extension: if ECT is not set on a segment,
* and we already seen ECT on a previous segment,
* it is probably a retransmit.
*/
if (tp->ecn_flags & TCP_ECN_SEEN) {
// tcp_enter_quickack_mode(sk, 2);
}
break;
case INET_ECN_CE:
// if (tcp_ca_needs_ecn(sk))
// tcp_ca_event(sk, CA_EVENT_ECN_IS_CE);
if (!(tp->ecn_flags & TCP_ECN_DEMAND_CWR)) {
/* Better not delay acks, sender can have a very low cwnd */
// tcp_enter_quickack_mode(sk, 2);
tp->ecn_flags |= TCP_ECN_DEMAND_CWR;
}
tp->ecn_flags |= TCP_ECN_SEEN;
break;
default:
// if (tcp_ca_needs_ecn(sk))
// tcp_ca_event(sk, CA_EVENT_ECN_NO_CE);
tp->ecn_flags |= TCP_ECN_SEEN;
break;
}
}
static void tcp_ecn_check_ce(struct sock *sk, const struct sk_buff *skb)
{
if (tcp_sk(sk)->ecn_flags & TCP_ECN_OK)
__tcp_ecn_check_ce(sk, skb);
}
[[rc::parameters("flags : tcp_ecn_flags", "psk : loc", "hdr : tcp_header", "phdr : loc",
"b : bool")]]
[[rc::args("psk @ &own<flags @ tcp_sock>", "phdr @ &own<hdr @ tcphdr>")]]
[[rc::requires("{bitfield_wf flags}")]]
[[rc::requires("{b = (ecn_ok flags) && (negb (tcp_ece hdr) || tcp_cwr hdr)}")]]
[[rc::ensures("own psk : {flags <| ecn_ok := negb b && (ecn_ok flags) |>} @ tcp_sock")]]
[[rc::ensures("own phdr : hdr @ tcphdr")]]
static void tcp_ecn_rcv_synack(struct tcp_sock *tp, const struct tcphdr *th)
{
if ((tp->ecn_flags & TCP_ECN_OK) && (!th->ece || th->cwr))
tp->ecn_flags &= ~TCP_ECN_OK;
}
[[rc::parameters("flags : tcp_ecn_flags", "psk : loc", "hdr : tcp_header", "phdr : loc",
"b : bool")]]
[[rc::args("psk @ &own<flags @ tcp_sock>", "phdr @ &own<hdr @ tcphdr>")]]
[[rc::requires("{bitfield_wf flags}")]]
[[rc::requires("{b = (ecn_ok flags) && (negb (tcp_ece hdr) || negb (tcp_cwr hdr))}")]]
[[rc::ensures("own psk : {flags <| ecn_ok := negb b && (ecn_ok flags) |>} @ tcp_sock")]]
[[rc::ensures("own phdr : hdr @ tcphdr")]]
static void tcp_ecn_rcv_syn(struct tcp_sock *tp, const struct tcphdr *th)
{
if ((tp->ecn_flags & TCP_ECN_OK) && (!th->ece || !th->cwr))
tp->ecn_flags &= ~TCP_ECN_OK;
}
[[rc::parameters("flags : tcp_ecn_flags", "psk : loc", "hdr : tcp_header", "phdr : loc")]]
[[rc::args("psk @ &own<flags @ tcp_sock>", "phdr @ &own<hdr @ tcphdr>")]]
[[rc::requires("{bitfield_wf flags}")]]
[[rc::returns("{(tcp_ece hdr) && negb (tcp_syn hdr) && (ecn_ok flags)} @ boolean<bool_it>")]]
static bool tcp_ecn_rcv_ecn_echo(const struct tcp_sock *tp, const struct tcphdr *th)
{
if (th->ece && !th->syn && (tp->ecn_flags & TCP_ECN_OK))
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment