arxpy.smt.verification_differential module

Verify characteristics found by the SMT solver.

To this end, a characteristic is split into sub-characteristics where each sub-ch has up to MAX_WEIGHT weight.

arxpy.smt.verification_differential.bv2ccode(bv)

Convert a bit-vector type to C code.

Parameters

bv – the bit-vector Term to convert

>>> from arxpy.bitvector.core import Constant, Variable
>>> from arxpy.bitvector.operation import RotateLeft
>>> from arxpy.smt.verification_differential import bv2ccode
>>> x, y = Variable("x", 8), Variable("y", 8)
>>> bv2ccode(x | y)
'x | y'
>>> bv2ccode(x + y)
'(x + y) & 255'
>>> bv2ccode(RotateLeft(x, 1))
'((x << 1) | (x >> 7)) & 255'
>>> bv2ccode((~x) + y)
Traceback (most recent call last):
...
ValueError: nested bit-vector operations are not supported

arxpy.smt.verification_differential.ssa2ccode(ssa, diff_type)

Return the C code to compute a differential probability over a function in ssa form.

>>> from arxpy.differential.difference import XorDiff, RXDiff
>>> from arxpy.primitives.chaskey import ChaskeyPi
>>> from arxpy.smt.verification_differential import ssa2ccode
>>> ChaskeyPi.set_rounds(1)
>>> ssa = ChaskeyPi.ssa(["v0", "v1", "v2", "v3"], "x")  
>>> header, source = ssa2ccode(ssa, XorDiff)
>>> print(header)
static unsigned long get_num_valid_pairs(uint32_t input_diff[], uint32_t output_diff[], unsigned long pair_samples, unsigned int seed);
>>> print(source)  
void eval(uint32_t v0, uint32_t v1, uint32_t v2, uint32_t v3, uint32_t* x7, uint32_t* x12, uint32_t* x13, uint32_t* x9){
    uint32_t x0 = (v0 + v1) & 4294967295;
    uint32_t x1 = ((v1 << 5) | (v1 >> 27)) & 4294967295;
    uint32_t x2 = x0 ^ x1;
    uint32_t x3 = ((x0 << 16) | (x0 >> 16)) & 4294967295;
    uint32_t x4 = (v2 + v3) & 4294967295;
    uint32_t x5 = ((v3 << 8) | (v3 >> 24)) & 4294967295;
    uint32_t x6 = x4 ^ x5;
    *x7 = (x3 + x6) & 4294967295;
    uint32_t x8 = ((x6 << 13) | (x6 >> 19)) & 4294967295;
    *x9 = *x7 ^ x8;
    uint32_t x10 = (x2 + x4) & 4294967295;
    uint32_t x11 = ((x2 << 7) | (x2 >> 25)) & 4294967295;
    *x12 = x10 ^ x11;
    *x13 = ((x10 << 16) | (x10 >> 16)) & 4294967295;
};
static unsigned long get_num_valid_pairs(uint32_t input_diff[], uint32_t output_diff[], unsigned long pair_samples, unsigned int seed){
    if (seed == 0) srand((unsigned int) time (NULL));
    else srand(seed);
    unsigned long num_valid_pairs = 0;
    unsigned long i = 0;
    unsigned int j = 0;
    uint32_t input1[4];
    uint32_t input2[4];
    uint32_t output1[4];
    uint32_t output2[4];
    for (; i < pair_samples; ++i) {
        for (j = 0; j < 4; ++j) {
            input1[j] = rand();
            input2[j] = input1[j] ^ input_diff[j];
        }
        eval(input1[0], input1[1], input1[2], input1[3], &output1[0], &output1[1], &output1[2], &output1[3]);
        eval(input2[0], input2[1], input2[2], input2[3], &output2[0], &output2[1], &output2[2], &output2[3]);
        for (j = 0; j < 4; ++j) {
            if ( (output1[j] ^ output2[j]) != output_diff[j] ) break;
            if (j == 4 - 1) num_valid_pairs += 1;
        }
    }
    return num_valid_pairs;
}
>>> header, source = ssa2ccode(ssa, RXDiff)
>>> print(header)
static unsigned long get_num_valid_pairs(uint32_t input_diff[], uint32_t output_diff[], unsigned long pair_samples, unsigned int seed);
>>> print(source)  
void eval(uint32_t v0, uint32_t v1, uint32_t v2, uint32_t v3, uint32_t* x7, uint32_t* x12, uint32_t* x13, uint32_t* x9){
    uint32_t x0 = (v0 + v1) & 4294967295;
    uint32_t x1 = ((v1 << 5) | (v1 >> 27)) & 4294967295;
    uint32_t x2 = x0 ^ x1;
    uint32_t x3 = ((x0 << 16) | (x0 >> 16)) & 4294967295;
    uint32_t x4 = (v2 + v3) & 4294967295;
    uint32_t x5 = ((v3 << 8) | (v3 >> 24)) & 4294967295;
    uint32_t x6 = x4 ^ x5;
    *x7 = (x3 + x6) & 4294967295;
    uint32_t x8 = ((x6 << 13) | (x6 >> 19)) & 4294967295;
    *x9 = *x7 ^ x8;
    uint32_t x10 = (x2 + x4) & 4294967295;
    uint32_t x11 = ((x2 << 7) | (x2 >> 25)) & 4294967295;
    *x12 = x10 ^ x11;
    *x13 = ((x10 << 16) | (x10 >> 16)) & 4294967295;
};
static unsigned long get_num_valid_pairs(uint32_t input_diff[], uint32_t output_diff[], unsigned long pair_samples, unsigned int seed){
    if (seed == 0) srand((unsigned int) time (NULL));
    else srand(seed);
    unsigned long num_valid_pairs = 0;
    unsigned long i = 0;
    unsigned int j = 0;
    uint32_t input1[4];
    uint32_t input2[4];
    uint32_t output1[4];
    uint32_t output2[4];
    for (; i < pair_samples; ++i) {
        for (j = 0; j < 4; ++j) {
            input1[j] = rand();
            input2[j] = ( ((input1[j] << 1) | (input1[j] >> 31)) ^ input_diff[j] ) & 4294967295;
        }
        eval(input1[0], input1[1], input1[2], input1[3], &output1[0], &output1[1], &output1[2], &output1[3]);
        eval(input2[0], input2[1], input2[2], input2[3], &output2[0], &output2[1], &output2[2], &output2[3]);
        for (j = 0; j < 4; ++j) {
            if ( (( ((output1[j] << 1) | (output1[j] >> 31)) ^ output2[j] ) & 4294967295) != output_diff[j] ) break;
            if (j == 4 - 1) num_valid_pairs += 1;
        }
    }
    return num_valid_pairs;
}

arxpy.smt.verification_differential.relatedssa2ccode(ssa1, ssa2, diff_type)

Return the C code to compute a differential probability over a (related) function in ssa form.

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.primitives.chaskey import ChaskeyPi
>>> from arxpy.smt.verification_differential import relatedssa2ccode
>>> ChaskeyPi.set_rounds(1)
>>> ssa1 = ChaskeyPi.ssa(["v0", "v1", "v2", "v3"], "x")  
>>> ssa2 = dict(ssa1)
>>> ssa2["assignments"] = list(ssa2["assignments"])
>>> ssa2["assignments"].append([ssa2["output_vars"][0], ssa2["output_vars"][0]])
>>> header, source = relatedssa2ccode(ssa1, ssa2, XorDiff)
>>> print(header)
static unsigned long get_num_valid_pairs(uint32_t input_diff[], uint32_t output_diff[], unsigned long pair_samples, unsigned int seed);
>>> print(source)  
void eval1(uint32_t v0, uint32_t v1, uint32_t v2, uint32_t v3, uint32_t* x7, uint32_t* x12, uint32_t* x13, uint32_t* x9){
    uint32_t x0 = (v0 + v1) & 4294967295;
    uint32_t x1 = ((v1 << 5) | (v1 >> 27)) & 4294967295;
    uint32_t x2 = x0 ^ x1;
    uint32_t x3 = ((x0 << 16) | (x0 >> 16)) & 4294967295;
    uint32_t x4 = (v2 + v3) & 4294967295;
    uint32_t x5 = ((v3 << 8) | (v3 >> 24)) & 4294967295;
    uint32_t x6 = x4 ^ x5;
    *x7 = (x3 + x6) & 4294967295;
    uint32_t x8 = ((x6 << 13) | (x6 >> 19)) & 4294967295;
    *x9 = *x7 ^ x8;
    uint32_t x10 = (x2 + x4) & 4294967295;
    uint32_t x11 = ((x2 << 7) | (x2 >> 25)) & 4294967295;
    *x12 = x10 ^ x11;
    *x13 = ((x10 << 16) | (x10 >> 16)) & 4294967295;
};
void eval2(uint32_t v0, uint32_t v1, uint32_t v2, uint32_t v3, uint32_t* x7, uint32_t* x12, uint32_t* x13, uint32_t* x9){
    uint32_t x0 = (v0 + v1) & 4294967295;
    uint32_t x1 = ((v1 << 5) | (v1 >> 27)) & 4294967295;
    uint32_t x2 = x0 ^ x1;
    uint32_t x3 = ((x0 << 16) | (x0 >> 16)) & 4294967295;
    uint32_t x4 = (v2 + v3) & 4294967295;
    uint32_t x5 = ((v3 << 8) | (v3 >> 24)) & 4294967295;
    uint32_t x6 = x4 ^ x5;
    *x7 = (x3 + x6) & 4294967295;
    uint32_t x8 = ((x6 << 13) | (x6 >> 19)) & 4294967295;
    *x9 = *x7 ^ x8;
    uint32_t x10 = (x2 + x4) & 4294967295;
    uint32_t x11 = ((x2 << 7) | (x2 >> 25)) & 4294967295;
    *x12 = x10 ^ x11;
    *x13 = ((x10 << 16) | (x10 >> 16)) & 4294967295;
    *x7 = *x7;
};
static unsigned long get_num_valid_pairs(uint32_t input_diff[], uint32_t output_diff[], unsigned long pair_samples, unsigned int seed){
    if (seed == 0) srand((unsigned int) time (NULL));
    else srand(seed);
    unsigned long num_valid_pairs = 0;
    unsigned long i = 0;
    unsigned int j = 0;
    uint32_t input1[4];
    uint32_t input2[4];
    uint32_t output1[4];
    uint32_t output2[4];
    for (; i < pair_samples; ++i) {
        for (j = 0; j < 4; ++j) {
            input1[j] = rand();
            input2[j] = input1[j] ^ input_diff[j];
        }
        eval1(input1[0], input1[1], input1[2], input1[3], &output1[0], &output1[1], &output1[2], &output1[3]);
        eval2(input2[0], input2[1], input2[2], input2[3], &output2[0], &output2[1], &output2[2], &output2[3]);
        for (j = 0; j < 4; ++j) {
            if ( (output1[j] ^ output2[j]) != output_diff[j] ) break;
            if (j == 4 - 1) num_valid_pairs += 1;
        }
    }
    return num_valid_pairs;
}

arxpy.smt.verification_differential.compile_run_empirical_weight(ccode, module_name, input_diff, output_diff, target_weight, verbose=False)

Compile and execute the C code to compute the empirical weight

>>> from arxpy.differential.difference import XorDiff, RXDiff
>>> from arxpy.primitives.chaskey import ChaskeyPi
>>> from arxpy.smt.verification_differential import ssa2ccode, compile_run_empirical_weight
>>> ChaskeyPi.set_rounds(1)
>>> ssa = ChaskeyPi.ssa(["v0", "v1", "v2", "v3"], "x")  
>>> header, source = ssa2ccode(ssa, XorDiff)
>>> ind, outd, tw = [0, 0, 0, 0], [0, 0, 0, 0], 2
>>> compile_run_empirical_weight([header, source], "_libverChaskeyPi", ind, outd, tw)
0.0
>>> ind, outd, tw = [0, 0, 0, 0], [0, 0, 0, 1], 2
>>> compile_run_empirical_weight([header, source], "_libverChaskeyPi", ind, outd, tw)
inf
>>> header, source = ssa2ccode(ssa, RXDiff)
>>> ind, outd, tw = [0, 0, 0, 0], [0, 0, 0, 0], 8
>>> 4 <= compile_run_empirical_weight([header, source], "_libverChaskeyPi", ind, outd, tw) <= 8
True
>>> ind, outd, tw = [0, 0, 0, 0], [1, 1, 1, 1], 8
>>> compile_run_empirical_weight([header, source], "_libverChaskeyPi", ind, outd, tw)
inf

arxpy.smt.verification_differential.fast_empirical_weight(ch_found, verbose_lvl=0, debug=False, filename=None)

Computes the empirical weight of the model using C code.

If filename is not None, the output will be printed to the given file rather than the to stdout.

The argument verbose_lvl can take an integer between 0 (no verbose) and 3 (full verbose).

>>> from arxpy.differential.difference import XorDiff, RXDiff
>>> from arxpy.differential.characteristic import BvCharacteristic
>>> from arxpy.primitives.chaskey import ChaskeyPi
>>> from arxpy.smt.search_differential import SearchCh
>>> from arxpy.smt.verification_differential import fast_empirical_weight
>>> ChaskeyPi.set_rounds(2)
>>> ch = BvCharacteristic(ChaskeyPi, XorDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> search_problem = SearchCh(ch)
>>> ch_found = search_problem.solve(0)
>>> ch_found.ch_weight
0x04
>>> 3 <= fast_empirical_weight(ch_found) <= 5
True
>>> ChaskeyPi.set_rounds(1)
>>> ch = BvCharacteristic(ChaskeyPi, RXDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> ic = [operation.BvComp(0, d.val) for d in ch.input_diff]
>>> ic += [operation.BvComp(0, d[1].val) for d in ch.output_diff]
>>> ch_found = SearchCh(ch, allow_zero_input_diff=True, initial_constraints=ic).solve(5)
>>> ch_found.ch_weight
0x05
>>> 4 - 1 <= fast_empirical_weight(ch_found) <= 8
True