| lists.openwall.net | lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC | |
|
Open Source and information security mailing list archives
| ||
|
Date: Wed, 31 Aug 2022 11:19:07 +0800
From: Shung-Hsi Yu <shung-hsi.yu@...e.com>
To: bpf@...r.kernel.org, linux-kernel@...r.kernel.org
Cc: "Alexei Starovoitov" <ast@...nel.org>,
"Daniel Borkmann" <daniel@...earbox.net>,
"John Fastabend" <john.fastabend@...il.com>,
Shung-Hsi Yu <shung-hsi.yu@...e.com>
Subject: [RFC bpf-next 2/2] proof for the safe usage of tnum_in()
This commit is not meant to be merged, merely as a display of proof
about the claims in previous commit that tnum_in() can be trusted when
used in the following form:
- tnum_in(tnum_const(), ...)
- tnum_in(tnum_range(0, 2**n - 1), ...)
- tnum_in(tnum_range(2**n, 2**(n+1) - 1), ...)
Note that this only proves that tnum_in() can be trusted when it returns
true, and proof nothing about whether it's trustworthy or not when it
returns false; the latter is still being worked on.
Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@...e.com>
---
tnum_in.py | 158 +++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 158 insertions(+)
create mode 100755 tnum_in.py
diff --git a/tnum_in.py b/tnum_in.py
new file mode 100755
index 000000000000..e4567bda51c4
--- /dev/null
+++ b/tnum_in.py
@@ -0,0 +1,158 @@
+#!/usr/bin/env python3
+#
+# A proof on the property of tnum_in(tnum_range(a, b), ...) using the Z3
+# theorem prover
+#
+# Requires the z3 Python module (aka Z3Py), which can be installed with the
+# command `pip3 install z3-solver`
+#
+from uuid import uuid4
+from z3 import And, BitVec, BitVecs, BitVecVal, Extract, If, Implies, Or, ULE, UGT, ZeroExt, prove
+
+
+class Tnum:
+ """A model of tristate number use in Linux kernel's BPF verifier.
+
+ Largely based on the "Sound, Precise, and Fast Abstract Interpretation with
+ Tristate Numbers" paper <https://arxiv.org/abs/2105.05398>.
+ """
+ SIZE = 64
+ def __init__(self, val=None, mask=None):
+ uid = uuid4() # Ensure that the BitVec are uniq, required by the Z3 solver
+ self.val = BitVec(f'Tnum-val-{uid}', bv=Tnum.SIZE) if val is None else val
+ self.mask = BitVec(f'Tnum-mask-{uid}', bv=Tnum.SIZE) if mask is None else mask
+
+ def contains(self, bitvec):
+ # Mask out the unknown bits, if what left is that same as value, then
+ # this that integer is represented by this tnum
+ return (~self.mask & bitvec) == self.val
+
+ def wellformed(self):
+ # Bit cannot be set in both val and mask, such tnum is not valid
+ return self.val & self.mask == BitVecVal(0, bv=Tnum.SIZE)
+
+
+def is_power_of_2(n):
+ return And(n != 0, n & (n-1) == 0)
+
+
+def fls64(bv):
+ size = Tnum.SIZE
+ num = BitVecVal(0, bv=Tnum.SIZE)
+ while size > 1:
+ half_size = size // 2
+ h = Extract(size - 1, half_size, bv)
+ bv = If(
+ h != 0,
+ h,
+ Extract(half_size - 1, 0, bv),
+ )
+ num += If(h != 0, BitVecVal(half_size, bv=Tnum.SIZE), BitVecVal(0, bv=Tnum.SIZE))
+ size = half_size
+
+ assert(size == 1) # Size is now 1
+ num += If(bv != 0, BitVecVal(1, bv=Tnum.SIZE), BitVecVal(0, bv=Tnum.SIZE))
+ return num
+
+
+def tnum_range(min_, max_): # Don't shadow built-in min & max
+ """tnum_range() implementation modeling what's found in the Linux Kernel"""
+ chi = min_ ^ max_
+ bits = fls64(chi)
+ delta = (BitVecVal(1, bv=Tnum.SIZE) << bits) - 1
+ too_large = UGT(bits, BitVecVal(Tnum.SIZE - 1, bv=Tnum.SIZE))
+
+ val = If(
+ too_large,
+ BitVecVal(0, bv=Tnum.SIZE),
+ min_ & ~delta,
+ )
+ mask = If(
+ too_large,
+ BitVecVal(-1, bv=Tnum.SIZE),
+ delta,
+ )
+ return Tnum(val=val, mask=mask)
+
+
+def tnum_in(a, b):
+ """tnum_in() implementation modeling what's found in the Linux Kernel"""
+ return If(
+ (b.mask & ~a.mask) != 0,
+ False,
+ a.val == (b.val & ~a.mask),
+ )
+
+
+# a, b, and x are integers which could be of any value
+a, b, x = BitVecs('a b x', bv=Tnum.SIZE)
+assumptions = []
+
+t = tnum_range(a, b) # Any possible range we could get out of tnum_range()
+assumptions += [
+ ULE(a, b), # a <= b
+]
+
+st = Tnum() # The second argument can be any tnum
+assumptions += [
+ st.wellformed(), # As long as it is a valid one
+ st.contains(x), # And contains the number x (that could be any integers)
+]
+
+condition = [
+ # When tnum_in() returns true
+ tnum_in(t, st) == True,
+]
+
+print("""\
+Trying to proof that tnum_in(tnum_range(a,b), ...) can always be trusted when
+it returns true...
+""")
+prove(
+ Implies(
+ # When using tnum_in(tnum_range(a, b), ...)
+ And(assumptions + condition),
+ # Try to prove that we can always trust it when it returns true
+ # That is, all number that the second argument can represent (i.e. x) is
+ # inclusively between a and b
+ And(ULE(a, x), ULE(x, b)),
+ )
+)
+print("")
+
+# Additional constrains, namely that the first argument need to be in the form of either
+# tnum_const()
+# or
+# tnum_range(0, 2**n - 1)
+# or
+# tnum_range(2**n, 2**(n+1) - 1)
+additional_assumptions = [
+ Or(
+ a == b, # since a == b, tnum_range(a, b) == tnum_const()
+ And(a == 0, is_power_of_2(b + 1)), # b is 2**n - 1
+ And(is_power_of_2(a), b == (a << 1) - 1) # a is 2**n and b is 2**(n+1) - 1
+ ),
+]
+
+print("""\
+Trying to proof that tnum_in(tnum_range(a,b), ...) can always be trusted when
+it returns true, again, but with constrains on a and b, namely the first
+argument of tnum_in() must be in one of the following forms:
+- tnum_in(tnum_const(), ...)
+- tnum_in(tnum_range(0, 2**n - 1), ...)
+- tnum_in(tnum_range(2**n, 2**(n+1) - 1), ...)
+""")
+prove(
+ Implies(
+ # When tnum_in() is used in the form of
+ # tnum_in(tnum_const(), ...)
+ # or
+ # tnum_in(tnum_range(0, 2**n - 1), ...)
+ # or
+ # tnum_in(tnum_range(2**n, 2**(n+1) - 1), ...)
+ And(assumptions + additional_assumptions + condition),
+ # Try to prove that we can always trust it when it returns true when the additional
+ # contrains above is inplace
+ And(ULE(a, x), ULE(x, b)),
+ )
+)
--
2.37.2
Powered by blists - more mailing lists