cascada.algebraic.opmodel module

Manipulate algebraic models of bit-vector operations.

`OpModel`	Represent algebraic models of bit-vector operations.
`BitModelId`	Represent the `BitValue` `algebraic.opmodel.OpModel` of `BvIdentity`.
`WordModelId`	Represent the `WordValue` `algebraic.opmodel.OpModel` of `BvIdentity`.
`BitModelBvAdd`	Represent the `BitValue` `algebraic.opmodel.OpModel` of `BvAdd`.
`BitModelBvSub`	Represent the `BitValue` `algebraic.opmodel.OpModel` of `BvSub`.

class cascada.algebraic.opmodel.OpModel(input_prop)[source]

Bases: cascada.abstractproperty.opmodel.OpModel

Represent algebraic models of bit-vector operations.

A (bit-vector) algebraic model of a bit-vector Operation \(f\) is a set of bit-vector constraints that models the propagation probability of value properties of \(f\). See Value.

An algebraic model is defined for a type of Value, such as BitValue or WordValue.

This class is not meant to be instantiated but to provide a base class for creating algebraic models.

Note

For all algebraic models, the pr_one_constraint method is equivalent to the validity_constraint method, and the weight of a valid propagation is always Constant(0, 1). This class implements the methods pr_one_constraint, bv_weight, max_weight, weight_width, decimal_weight, num_frac_bits and error, and subclasses only need to implement validity_constraint.

val_type: the type of Value (alias of abstractproperty.opmodel.OpModel.prop_type).

input_val: a list containing the Value of each bit-vector operand (alias of abstractproperty.opmodel.OpModel.input_prop).

pr_one_constraint(output_val)[source]

Return the probability-one constraint for a given output Property.

Return the constraint that evaluates to True if the input Property propagates to the given output Property with probability one.

This method returns a bit-vector expression that depends on the input property OpModel.input_prop and the output property output_prop and it is True if and only if the input property propagates to the output property with probability 1.

If both the input and output properties are constant values, this method returns the Constant 0b1 or 0b0 depending on whether the corresponding propagation has probability 1. Otherwise, this method returns a bit-vector Term containing the input and output properties as Variable objects.

bv_weight(output_val)[source]

Return the bit-vector weight for a given output Property.

The bit-vector weight is a bit-vector expression that depends on the input property OpModel.input_prop and the output property output_prop. This bit-vector function represents an approximation of the negative binary logarithm (weight) of the probability of the input property propagating to the output property.

Note

This method is optional and subclasses of OpModel don’t need to implement it (as opposed to OpModel.weight_constraint).

It is assumed that the corresponding propagation has non-zero probability.

If the input and output properties are constant values, this method returns a Constant of bit-size weight_width denoting the weight of the valid propagation. Otherwise, this method returns a bit-vector Term containing the input and output properties as Variable objects.

max_weight()[source]: Return the maximum value the weight variable can achieve in OpModel.weight_constraint.

weight_width()[source]: Return the width of the weight variable used OpModel.weight_constraint.

decimal_weight(output_val)[source]

Return the decimal.Decimal weight for a given constant output Property.

This method returns, as a decimal number, the weight (negative binary logarithm) of the probability of the input property propagating to the output property.

This method only works when the input property and the output property are constant values, but provides a better approximation than the bit-vector weight from OpModel.weight_constraint.

num_frac_bits()[source]

Return the number of fractional bits used in the weight variable of OpModel.weight_constraint.

If the number of fractional bits is k, then the bit-vector weight variable w of OpModel.weight_constraint represents the number 2^{-k} * bv2int(w). In particular, if k == 0, then w represents an integer number. Otherwise, the k least significant bits of w denote the fractional part of the number represented by w.

error()[source]

Return the maximum difference between OpModel.weight_constraint and the exact weight.

The exact weight is exact value (without error) of the negative binary logarithm (weight) of the propagation probability of \((\alpha, \beta)\).

Note

The exact weight can be computed in TestOpModelGeneric.get_empirical_weight_slow.

This method returns an upper bound (in absolute value) of the maximum difference (over all input and output properties) between the bit-vector weight from OpModel.weight_constraint and the exact weight.

Note that the exact weight might still differ from decimal_weight.

class cascada.algebraic.opmodel.BitModelId(input_prop)[source]

Bases: cascada.abstractproperty.opmodel.ModelIdentity, cascada.algebraic.opmodel.OpModel

Represent the BitValue algebraic.opmodel.OpModel of BvIdentity.

See also ModelIdentity.

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.algebraic.value import WordValue
>>> from cascada.algebraic.opmodel import WordModelId
>>> alpha, beta = WordValue(Variable("a", 4)), WordValue(Variable("b", 4))
>>> f = WordModelId(alpha)
>>> print(f.vrepr())
WordModelId(WordValue(Variable('a', width=4)))
>>> f.validity_constraint(beta)
a == b
>>> f.max_weight(), f.weight_width(), f.error(), f.num_frac_bits()
(0, 1, 0, 0)

val_type: alias of cascada.algebraic.value.WordValue

class cascada.algebraic.opmodel.BitModelBvAdd(input_prop)[source]

Bases: cascada.algebraic.opmodel.OpModel

Represent the BitValue algebraic.opmodel.OpModel of BvAdd.

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.algebraic.value import BitValue
>>> from cascada.algebraic.opmodel import BitModelBvAdd
>>> alpha = BitValue(Variable("a", 4)), BitValue(Variable("b", 4))
>>> f = BitModelBvAdd(alpha)
>>> print(f.vrepr())
BitModelBvAdd([BitValue(Variable('a', width=4)), BitValue(Variable('b', width=4))])
>>> f.max_weight(), f.weight_width(), f.error(), f.num_frac_bits()
(0, 1, 0, 0)

val_type: alias of cascada.algebraic.value.BitValue

op: alias of cascada.bitvector.operation.BvAdd

validity_constraint(output_val)[source]

Return the validity constraint for a given BitValue output.

This model is based on the fact that the \(n\)-bit modular addition \(x \boxplus y = z\) has the following implicit function \(x \oplus y \oplus z \oplus Q(x \oplus z, y \oplus z)\) where \(Q(x, y) = (0, x_0 \wedge y_0, (x_0 \wedge y_0) \oplus (x_1 \wedge y_1), \dots, (x_0 \wedge y_0) \oplus (x_1 \wedge y_1) \oplus \dots \oplus (x_{n-2} \wedge y_{n-2}))\)

Source: Implicit White-Box Implementations: White-Boxing ARX Ciphers.

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.algebraic.value import BitValue
>>> from cascada.algebraic.opmodel import BitModelBvAdd
>>> alpha = BitValue(Constant(0, 3)), BitValue(Constant(0, 3))
>>> f = BitModelBvAdd(alpha)
>>> beta = BitValue(Constant(0, 3))
>>> f.validity_constraint(beta)
0b1
>>> a0, a1, b = Variable("a0", 3), Variable("a1", 3), Variable("b", 3)
>>> alpha = BitValue(a0), BitValue(a1)
>>> f = BitModelBvAdd(alpha)
>>> beta = BitValue(b)
>>> result = f.validity_constraint(beta)
>>> result  
(0b0 == ((a0[0]) ^ (a1[0]) ^ (b[0]))) &
(0b0 == ((a0[1]) ^ (a1[1]) ^ (b[1]) ^ (((a0[0]) ^ (b[0])) & ((a1[0]) ^ (b[0]))))) &
(0b0 == ((a0[2]) ^ (a1[2]) ^ (b[2]) ^ (((a0[0]) ^ (b[0])) & ((a1[0]) ^ (b[0]))) ^ (((a0[1]) ^ (b[1])) & ((a1[1]) ^ (b[1])))))
>>> result.xreplace({a0: Constant(0, 3), a1: Constant(0, 3), b: Constant(0, 3)})
0b1
>>> a1 = Constant(0, 3)
>>> alpha = BitValue(a0), BitValue(a1)
>>> f = BitModelBvAdd(alpha)
>>> beta = BitValue(b)
>>> result = f.validity_constraint(beta)
>>> result  
(0b0 == ((a0[0]) ^ (b[0]))) &
(0b0 == ((a0[1]) ^ (b[1]) ^ (((a0[0]) ^ (b[0])) & (b[0])))) &
(0b0 == ((a0[2]) ^ (b[2]) ^ (((a0[0]) ^ (b[0])) & (b[0])) ^ (((a0[1]) ^ (b[1])) & (b[1]))))

See OpModel.validity_constraint for more information.

class cascada.algebraic.opmodel.BitModelBvSub(input_prop)[source]

Bases: cascada.algebraic.opmodel.OpModel

Represent the BitValue algebraic.opmodel.OpModel of BvSub.

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.algebraic.value import BitValue
>>> from cascada.algebraic.opmodel import BitModelBvSub
>>> alpha = BitValue(Variable("a", 4)), BitValue(Variable("b", 4))
>>> f = BitModelBvSub(alpha)
>>> print(f.vrepr())
BitModelBvSub([BitValue(Variable('a', width=4)), BitValue(Variable('b', width=4))])
>>> f.max_weight(), f.weight_width(), f.error(), f.num_frac_bits()
(0, 1, 0, 0)

The algebraic model of the modular substraction is based on BitModelBvAdd since ~(x - y) == ~x + y.

val_type: alias of cascada.algebraic.value.BitValue

op: alias of cascada.bitvector.operation.BvSub

validity_constraint(output_val)[source]

Return the validity constraint for a given BitValue output.

>>> from cascada.bitvector.core import Constant, Variable
>>> from cascada.algebraic.value import BitValue
>>> from cascada.algebraic.opmodel import BitModelBvSub
>>> alpha = BitValue(Constant(0, 3)), BitValue(Constant(0, 3))
>>> f = BitModelBvSub(alpha)
>>> beta = BitValue(Constant(0, 3))
>>> f.validity_constraint(beta)
0b1
>>> a0, a1, b = Variable("a0", 3), Variable("a1", 3), Variable("b", 3)
>>> alpha = BitValue(a0), BitValue(a1)
>>> f = BitModelBvSub(alpha)
>>> beta = BitValue(b)
>>> result = f.validity_constraint(beta)
>>> result  
(0b0 == (~(a0[0]) ^ (a1[0]) ^ ~(b[0]))) &
(0b0 == (~(a0[1]) ^ (a1[1]) ^ ~(b[1]) ^ ((~(a0[0]) ^ ~(b[0])) & ((a1[0]) ^ ~(b[0]))))) &
(0b0 == (~(a0[2]) ^ (a1[2]) ^ ~(b[2]) ^ ((~(a0[0]) ^ ~(b[0])) & ((a1[0]) ^ ~(b[0]))) ^ ((~(a0[1]) ^ ~(b[1])) & ((a1[1]) ^ ~(b[1])))))
>>> result.xreplace({a0: Constant(0, 3), a1: Constant(0, 3), b: Constant(0, 3)})
0b1
>>> a1 = Constant(0, 3)
>>> alpha = BitValue(a0), BitValue(a1)
>>> f = BitModelBvSub(alpha)
>>> beta = BitValue(b)
>>> result = f.validity_constraint(beta)
>>> result  
(0b0 == (~(a0[0]) ^ ~(b[0]))) &
(0b0 == (~(a0[1]) ^ ~(b[1]) ^ ((~(a0[0]) ^ ~(b[0])) & ~(b[0])))) &
(0b0 == (~(a0[2]) ^ ~(b[2]) ^ ((~(a0[0]) ^ ~(b[0])) & ~(b[0])) ^ ((~(a0[1]) ^ ~(b[1])) & ~(b[1]))))

See OpModel.validity_constraint for more information.