cascada.abstractproperty.characteristic module

Manage non-symbolic characteristics w.r.t an abstract property.

`EmpiricalWeightData`	Represent the auxiliary data of `empirical_ch_weight`.
`Characteristic`	Represent characteristics over bit-vector functions w.r.t some property.
`EncryptionCharacteristic`	Represent characteristics over encryption functions w.r.t some property.
`CipherCharacteristic`	Represent characteristics over ciphers w.r.t some property.

class cascada.abstractproperty.characteristic.EmpiricalWeightData(aux_weights, num_input_samples, seed, C_code, num_external_samples=None)[source]

Bases: object

Represent the auxiliary data of empirical_ch_weight.

This class stores the auxiliary data (the auxiliary empirical weights and the input parameters) of characteristic empirical weights computed through the method Characteristic.compute_empirical_ch_weight.

weight_avg_aux_prs: the negative binary logarithm (weight) of the average of the underlying probabilities of the auxiliary empirical weights

num_aux_weights: the total number of auxiliary weights computed (including weights with value math.inf)

num_inf_aux_weights: the number of auxiliary weights with value math.inf

num_input_samples: the number of inputs sampled

num_external_samples: the number of external samples used (equal to the number of auxiliary weights if there are two or more)

seed: the seed used to sample bit-vectors

C_code: whether the on-the-fly C implementations was used

aux_weights: the list of auxiliary empirical weights

vrepr()[source]

Return an executable string representation.

This method returns a string so that eval(self.vrepr()) returns a new EmpiricalWeightData object with the same content.

class cascada.abstractproperty.characteristic.Characteristic(input_prop, output_prop, assign_outprop_list, ch_model, external_props=None, free_props=None, empirical_ch_weight=None, empirical_data_list=None, is_valid=True)[source]

Bases: object

Represent characteristics over bit-vector functions w.r.t some property.

Given a BvFunction \(f\) and its SSA decomposition into a list of simple assignments \(x_{i+1} \leftarrow f_i(x_i)\), a characteristic is a trail of properties \((\Delta_{x_0} \mapsto \Delta_{x_1} \mapsto \dots \mapsto \Delta_{x_r})\) containing the input and output Property pair \((\Delta_{x_{i}}, \Delta_{x_{i+1}})\) of each assignment \(x_{i+1} \leftarrow f_i(x_i)\), where \(f_i\) is a bit-vector Operation. The initial property \(\Delta_{x_0}\) is called the input property of the characteristic, and the last property \(\Delta_{x_r}\) is called the output property of the characteristic.

If a BvFunction \(f\) contains external variables, recall the external variables appear in the SSA as input operands in some assignments. Thus, the properties associated to the external variables appear in the characteristic trail as input properties of those assignments.

Note

For example, given the function \(f(x) = (x \oplus 1) \boxplus z\) with external variable \(z\), a characteristic over \(f\) is a trail of properties given by 2 property pairs:

The first property pair \((\Delta_x, \Delta_{x'})\) is over the assignment \(x' \leftarrow f_0(x) = x \oplus 1\).
The second property pair \(((\Delta_{x'}, \Delta_z), \Delta_{x''})\) is over the assignment \(x'' \leftarrow f_1(x', z) = x' \boxplus z\).

The propagation probability of a characteristic, or simply the characteristic probability, is the product of the propagation probabilities of the Property pairs \((\Delta_{x_{i}} \mapsto \Delta_{x_{i+1}})\) over \(f_i\).

The propagation weight of a characteristic is the negative binary logarithm of the characteristic probability, that is, the sum of the propagation weights of the Property pairs \((\Delta_{x_{i}} \mapsto \Delta_{x_{i+1}})\).

Note

For a function \(f(x) = g(x, x)\) with duplicated input \(x\), if the property model of \(f\) is not implemented but the model of \(g\) is, then the property model of \(f\) is approximated with the model of \(g\).

For example, the XorDiff model of the unary operation \(f(x) = x \boxplus x\) is approximated by XorModelBvAdd with the same difference for the first and second operands.

The characteristic probability is an approximation of the propagation probability of the property pair \((\Delta_{x_0}, \Delta_{x_r})\) over \(f\), but the accuracy of this approximation varies depending on the Property type, the function \(f\) and the SSA decomposition of \(f\). For some properties such as Difference and LinearMask, if \(f\) has external variables then the characteristic probability approximates the propagation probability of \((\Delta_{x_0}, \Delta_{x_r})\) averaged over the set of all values of the external variables.

A Characteristic is defined for a abstractproperty.chmodel.ChModel (providing the type of Property, the BvFunction \(f\), the SSA decomposition, and the (symbolic) Property propagations over the non-trivial assignments as abstractproperty.opmodel.OpModel objects).

Note

A Characteristic object represents an instance of characteristic (where all the properties and weights are constant values), whereas a abstractproperty.chmodel.ChModel object represents the (symbolic) model of a characteristic.

A Characteristic also requires the values of the properties \(\Delta_{x_i}\) in the trail. The property values can be given as Constant objects or Property of Constant objects.

Note

To initialize a Characteristic, all the constant values of the input, output, external and assignment-output properties must be given, even for properties not affecting the trail. These free symbolic properties can be given in the free_props list to denote that their value does not affect the characteristic.

If the underlying bit-vector function does not have external variables, or the attribute external_var2prop of the underlying characteristic model maps all external variables to constant Property objects, then the initialization argument external_props can be omitted.

If the bit-vector function \(f\) of the given abstractproperty.chmodel.ChModel is a RoundBasedFunction including add_round_outputs calls in its eval, then the characteristic over each round can be obtaining by combining split and get_round_separators.

To initialize an invalid Characteristic (with zero characteristic probability), the initialization argument is_valid=False must be provided (by default, is_valid=True).

This class is not meant to be instantiated but to provide a base class for creating characteristic w.r.t some property, (see differential.characteristic.Characteristic, linear.characteristic.Characteristic or algebraic.characteristic.Characteristic for some examples).

ch_model: the underlying abstractproperty.chmodel.ChModel.

ch_weight: the decimal weight of the characteristic computed as the sum of assignment_weights.

assignment_weights: the decimal weight of the Property \((\Delta_{x_{i}} \mapsto \Delta_{x_{i+1}})\) over each non-trivial assignment \(x_{i+1} \leftarrow f_i(x_i)\), computed from the abstractproperty.opmodel.OpModel.decimal_weight method of the abstractproperty.opmodel.OpModel objects stored in tuple_assign_outprop2op_model.

empirical_ch_weight: the empirical weight of the characteristic (available after calling compute_empirical_ch_weight).

empirical_data_list: a list of EmpiricalWeightData objects containing the auxiliary data of the empirical weight (see also compute_empirical_ch_weight).

input_prop: a list of Property objects containing the (constant) input property.

output_prop: a list of Property objects containing the (constant) output property.

external_props: a list containing the (constant) Property of the external variables of the function.

tuple_assign_outprop2op_model: a tuple where each element is a pair containing: (1) the output (constant) Property \(\Delta_{x_{i+1}}\) of the non-trivial assignment \(x_{i+1} \leftarrow f_i(x_i)\) and (2) the abstractproperty.opmodel.OpModel of this assignment with a (constant) input Property \(\Delta_{x_{i}}\).

free_props: a list of (symbolic) Property objects of the ch_model, whose values do not affect the characteristic, and were replaced by constant properties in input_prop, output_prop, external_props or tuple_assign_outprop2op_model.

var_prop2ct_prop: a collections.OrderedDict mapping each symbolic Property in the trail to its constant property.

static get_properties_for_initialization(ch_model, var2ct, free_props=None)[source]

Return the properties needed to initialize a Characteristic object.

Given a abstractproperty.chmodel.ChModel and a dictionary mapping Variable objects (representing the symbolic properties) to their Constant values, this method returns the following objects: input_prop, output_prop, external_props and assign_outprop_list for the Characteristic.__init__ method.

Symbolic properties not affecting the characteristics can be given in free_props and they will be set to 0.

vrepr(ignore_external_props=False)[source]

Return an executable string representation.

This method returns a string so that eval(self.vrepr()) returns a new Characteristic object with the same content.

srepr()[source]

Return a short string representation of the characteristic.

The short representation includes the characteristic weight rounded up to 3 fractional digits (and similar for the empirical weight if defined) and the input and output properties, printed in hexadecimal but omitting the prefix 0x.

Doctest included in vrepr.

signature(ch_signature_type)[source]

Return the signature of the characteristic.

This method is similar that abstractproperty.chmodel.ChModel.signature but for non-symbolic characteristic.

split(prop_separators)[source]

Split into multiple Characteristic objects given the list of property separators.

Given the Characteristic \(c\), this method returns a list of characteristics \(c_1, c_2, ..., c_n\), such that their composition is equal to the main characteristic \(c\).

The argument prop_separators is a list containing lists of symbolic properties. The \(i\)-th property list denote the last properties of the \(i\)-th abstractproperty.chmodel.ChModel. In other words, the \((i+1)\)-th characteristic immediately starts after the last property in prop_separators[i].

To split into \(n\) characteristics, prop_separators must contain \(n-1\) lists, as the property list of the last characteristic is not given (its last properties are the output properties of the main characteristic).

This method internally calls abstractproperty.chmodel.ChModel.split to split the underlying characteristic model ch_model.

compute_empirical_ch_weight(num_input_samples=None, num_external_samples=None, split_by_max_weight=None, split_by_rounds=False, seed=None, C_code=False, num_parallel_processes=None)[source]

Compute and store the empirical weight.

Given the characteristic \((\Delta_{x_0} \mapsto \Delta_{x_1} \mapsto \dots \mapsto \Delta_{x_r})\) over \(f\), the empirical weight is an estimation of the propagation weight of \((\Delta_{x_0}, \Delta_{x_r})\) empirically obtained by evaluating \(f\) for many sampled inputs and external samples (if \(f\) has external variables).

Note

The empirical weight only takes into account the input and output properties; intermediate properties in the trail are ignored.

Note it is possible for the empirical weight to be smaller than ch_weight in some cases and to be larger in others.

If \(f\) does not have external variables, in general (depends on the Property) the empirical weight is computed by \(f\)-evaluating num_input_samples random inputs satisfying input_prop and counting the number of outputs satisfying output_prop. This procedure is called here the basic subroutine, and it varies from Property to Property.

If \(f\) contains external variables, the basic subroutine is repeated num_external_samples times, where the external variables are fixed in each iteration to random values satisfying external_props. As a result, num_external_samples auxiliary empirical weights are obtained, and the final empirical weight is taken as the negative binary logarithm of the average of the underlying probabilities of the auxiliary empirical weights.

Note

The average is taken on the underlying probabilities since these probabilities might be zero in some cases (and their corresponding weights math.inf).

This method computes the empirical weight and stores it in empirical_ch_weight. Moreover, the input parameters and the auxiliary weights is stored in empirical_data_list as a list of EmpiricalWeightData objects. This list contains multiple objects only if the characteristic was split into multiple ones (see below); in that case, this list contains an EmpiricalWeightData object for each characteristic the main one was split into.

If one of the arguments split_by_max_weight or split_by_rounds is enabled, the characteristic is first split into multiple characteristics and then the empirical weights of the new characteristics are computed (by calling compute_empirical_ch_weight on each new characteristic). The final empirical weight is taken as the sum of the empirical weights of the new characteristics. If the empirical weight of one of the new characteristics is math.inf, the ongoing computations are aborted and the unfinished empirical weights are stored as EmpiricalWeightData objects with math.inf weight, num_input_samples=0 and num_external_samples=0.

Note

When the characteristic is split, the final empirical weight is more an approximation of the characteristic weight that the weight of the input-output pair, as now the empirical weight computation also takes into account the intermediate properties that are part of the input and output properties of the new characteristics are also taken into account.

Parameters

num_input_samples – the number of inputs to sample.
num_external_samples – the number of external samples (set to 0 if the underlying bit-vector function does not contain external variables).
split_by_max_weight – an optional number; if given, computes the empirical weight by splitting the characteristic into multiple characteristics (each one with maximum weight less than max(split_by_max_weight, max(self.assignment_weights)) ).
split_by_rounds – if True, computes the empirical weight by splitting the characteristic into multiple characteristics, each one covering one round (only available if the underlying function of the characteristic model is a RoundBasedFunction including add_round_outputs calls in its eval)
seed – the seed for sampling random bit-vectors
C_code – whether to use a faster C implementation generated on-the-fly
num_parallel_processes – if not None and C_code=True, the auxiliary empirical weights are computed in parallel (using the given number of worker processes)

classmethod random(ch_model, seed, external_props=None)[source]

Return a random Characteristic with given abstractproperty.chmodel.ChModel.

Parameters

ch_model – the underlying characteristic model
seed – the seed used to sample bit-vectors
external_props – a list containing the (constant) Property of the external variables or None to sample random properties for the external variables.

get_formatted_logged_msgs()[source]

Return the list of logged messages.

If self.ch_model.func includes log_msg calls in its eval, this method return the list of messages logged with the format field objects applied. Otherwise, an empty list is returned.

In the first case, the Variable objects of self.ch_model.ssa appearing in the format field objects are replaced with their associated constant Property objects.

get_round_separators()[source]

Return the round separators if self.ch_model.func is a RoundBasedFunction.

If self.ch_model.func includes add_round_outputs calls in its eval, this method returns a list with the (symbolic) round Property outputs delimiting the rounds. Otherwise, None is returned.

In the first case, this list contains num_rounds - 1 entries, where the i-th entry is the list of (symbolic) Property outputs of the i-th round. In particular, the output properties of the last round are not included in this list.

The list returned by this method is meant to be used as the argument of Characteristic.split to get the Characteristic object of each round.

dotprinting(repeat=True, vrepr_label=False, **kwargs)[source]

Return the DOT description of the expression tree of tuple_assign_outprop2op_model.