Encoding Bitwise Functions as Polynomials
Introduction
Symbolic solvers and theorem provers are powerful tools that allow the user to prove the satisfiability of a collection of statements and can even provide concrete values that satisfy them. Common applications of solvers are solving a function for its inputs given its outputs or proving specific properties.
Interestingly, while building this solver, I realized that I had technically built an automated theorem prover (ATP). As I was exploring the Wikipedia rabbit hole for ATPs, I came across Zhegalkin polynomials[1], and realized that I had rediscovered them.
Polynomials
Definition
Interpretation as structures
Composition
Solving with polynomials
def f(a):
a -= 53
for i in range(1, 17):
if not i % 7:
a *= i*a
elif i == 5:
a += 20
else:
a += i+1
a -= 5
return a - 107└─$ poly = f(x)
<Polynomial: (686)*x^4 + (-115248)*x^3 + (7267288)*x^2 + (-203857248)*x + 2146394847, coeff_ring=ZZ>Mathematically representing bitwise functions
Binary operations over bits
Symbolic representation using polynomials
Imagine we're working with this function:
def f(a, b):
c = a ^ b
return (c | a) & (b @ ~a) & b<SymBit: value=<Polynomial: (a + 1)*b, coeff_ring=ZZ/(ZZ(2))[a]>>Bit vectors
Solving symbolic expressions
Defining the problem
Creating the algorithm
The constraint system
Analyzing the symbolic representation
Before we compile more complex functions, we should analyze the properties of our representation to get a good idea of its strengths and limitations.
Branchless
Cardinality of bitwise functions
Constructing an ALU
Introduction
An arithmetic logic unit (ALU) is the part of a CPU responsible for various arithmetic operations. Generally, it performs addition, subtraction, multiplication, division, left rotates, right rotates, etc.
Conceptually, building the ALU using the symbolic compiler is simple. We just need to implement its hardware algorithms using bitwise functions. I will not be going over implementing each function because the algorithms are well known. However, a problem quickly arises from using the symbolic representation: conditionals. Recall from the analysis that we are not allowed to branch. Is building the ALU even still possible? Well yes, we just have to encode the result of the conditional in a branchless way.
Branchless conditionals
Implementation
Demonstration
Conclusion and closing remarks
Polynomials are a versatile and powerful tool in mathematics. Encoding problems in polynomials allows us to apply centuries of reasoning to them. Using some basic math, we were able to represent an entire ALU and solve it for specific outputs. This is a simple study implementation meant to showcase one way to solve bitwise functions, so the current implementation is quite slow. There are many areas to explore in optimizing both the compiler and solver.
Footnotes
1. https://en.wikipedia.org/wiki/Zhegalkin_polynomial
2. https://en.wikipedia.org/wiki/Polynomial
3. https://math.stackexchange.com/questions/2418323/how-many-functions-have-an-n-bit-input-and-m-bit-output
Credits
This article was written by Dani Cronce, a Senior Security Consultant here at Leviathan. You can get in touch with Dani on her LinkedIn profile.