sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
184 stars 169 forks source link

Fix two invalid dereferences in if_etherip-fixed-double-free #1232

Closed mchalupa closed 3 years ago

mchalupa commented 3 years ago

1) ipcounters global variable is not initialized and therefore is null when accessed in counters_inc() (called from main -> ip_deliver -> ipstat_inc -> counters_inc).

2) ip_deliver() is called from main with nxt = 0 and af = AF_INET6, which causes to take the 0th element of inet6sw (line 631) which has pr_input set to null. Then this null is dereferenced on line 634.

Both invalid dereferences may be hit if you replace the nondet values with the following concrete values:

diff --git a/c/openbsd-6.2/if_etherip-fixed-double-free.i b/c/openbsd-6.2/if_etherip-fixed-double-free.i
index 93be21b267..fd164a049b 100644
--- a/c/openbsd-6.2/if_etherip-fixed-double-free.i
+++ b/c/openbsd-6.2/if_etherip-fixed-double-free.i
@@ -407,7 +407,7 @@ void assume_abort_if_not(int cond) {
     abort();
   }
 }
-_Bool __VERIFIER_nondet_bool(void);
+_Bool __VERIFIER_nondet_bool(void) { return 0; }
 int __VERIFIER_nondet_int(void);
 void __VERIFIER_atomic_begin(void);
 void __VERIFIER_atomic_end(void);
@@ -705,14 +705,14 @@ int etherip_allow;
 int main(void) {
   struct mbuf *m;
   int len, off;
-  etherip_allow = __VERIFIER_nondet_int();
+  etherip_allow = 0;
   ip_init();
   m = m_gethdr((0x0001), (0x0002));
-  len = __VERIFIER_nondet_int();
+  len = 1;
   assume_abort_if_not(len > 0);
   assume_abort_if_not(len <=
                       ((256 - sizeof(struct m_hdr)) - sizeof(struct pkthdr)));
-  off = __VERIFIER_nondet_int();
+  off = 1;
   assume_abort_if_not(off > 0);
   assume_abort_if_not(off <= len);
   m->m_hdr.mh_len = m->M_dat.MH.MH_pkthdr.len = len;
@@ -5742,7 +5742,7 @@ int ip6_output(struct mbuf *a, struct ip6_pktopts *b, struct route_in6 *c,
   }
   return 0;
 }
-unsigned int rtable_l2(unsigned int a) { return __VERIFIER_nondet_int(); }
+unsigned int rtable_l2(unsigned int a) { return 0; }
 int etherip_input(struct mbuf **a, int *b, int c, int d) { return 257; }
 void ml_enqueue(struct mbuf_list *a, struct mbuf *b) {}
 void if_input(struct ifnet *a, struct mbuf_list *b) {}