ExpoSE

ExpoSE copied to clipboard

I'm trying to test a small (non-cryptographic) hash function (NB: the actual function I want to test uses charCodeAt(), but since this isn't supported in ExpoSE, I switched to arrays of ints with some reasonable constraints):

"use strict";

var S$ = require('S$');

function obfuscateWord(e) {
    let t = 0x17ed2e7f1ccbb000;
    for (let n = 0; n < e.length; n++) t = 33 * t ^ e[n];
    return t
}

var a = S$.symbol("A", [0] );
S$.assume(a.length < 5);
S$.assume(a.length > 1);
for (var i = 0; i < a.length; i++) {
    S$.assume(a[i] > 96);  // a
    S$.assume(a[i] < 123); // z
}

// 69712246 is the hash of "test"
if (obfuscateWord(a) == 69712246) {
    throw 'Reachable';
}

When I run this through ExpoSE with EXPOSE_PRINT_PATHS=1, it never finds the "Reachable" line (which can be reached with the input test, i.e. [116, 101, 115, 116]. Instead it generates lots of test cases with this exception (full log attached):

[!] Uncaught exception RangeError [ERR_OUT_OF_RANGE]: error setting argument 2 - The value of "value" is out of range. It must be >= -2147483648 and <= 2147483647. Received 56_894_816_742_442_910_000 Stack: RangeError [ERR_OUT_OF_RANGE]: The value of "value" is out of range. It must be >= -2147483648 and <= 2147483647. Received 56_894_816_742_442_910_000
    at checkInt (internal/buffer.js:69:11)  
    at writeU_Int32LE (internal/buffer.js:689:3)
    at Buffer.writeInt32LE (internal/buffer.js:858:10)
    at Object.set (/home/moyix/git/ExpoSE/Analyser/node_modules/z3javascript/node_modules/ref-napi/lib/ref.js:932:50)                                                                                                                                                      
    at Object.set (/home/moyix/git/ExpoSE/Analyser/node_modules/z3javascript/node_modules/ref-napi/lib/ref.js:492:10)
    at Object.alloc (/home/moyix/git/ExpoSE/Analyser/node_modules/z3javascript/node_modules/ref-napi/lib/ref.js:526:13)
    at Context.proxy (/home/moyix/git/ExpoSE/Analyser/node_modules/z3javascript/node_modules/ffi-napi/lib/_foreign_function.js:50:28) 
    at Context.Z3.<computed> (/home/moyix/git/ExpoSE/Analyser/node_modules/z3javascript/bin/package.js:811:32)
    at Context._buildConst (/home/moyix/git/ExpoSE/Analyser/node_modules/z3javascript/bin/Context.js:76:27)
    at Context._build (/home/moyix/git/ExpoSE/Analyser/node_modules/z3javascript/bin/Context.js:67:31)
[!] ====== EXITING SCRIPT /home/moyix/git/ExpoSE/obfuscate_short.js depth 0 ======

Full log: expose_error.txt

Any idea what is going wrong here? Or did I do something wrong with the constraints?

Ah, ok. The problem is that 0x17ed2e7f1ccbb000*33 is too big to turn into a 32-bit int. In JS I think this is silently handled but adding a & 0xffffffff there helps ExpoSE get past that point. Unfortunately, after that it seems that XOR is not supported:

[!] Symbolic execution does not support operand ^, concretizing.

Oh, I forgot to add support for ^.

You could try adding support for xor through real to int conversion around here, see the >> and << operators for an example. If it works please let me know https://github.com/ExpoSEJS/ExpoSE/blob/20e2357764e6b007da4206ae89312722e58c33f0/Analyser/src/SymbolicState.js#L452. It might be a bit slow though because converting reals to ints in SMT is expensive.

I'm not sure if I added support for xor to z3javascript either but the change there is quite straightforward too.

Thanks, Blake

On Tue, 31 Aug 2021, 00:41 Brendan Dolan-Gavitt, @.***> wrote:

Ah, ok. The problem is that 0x17ed2e7f1ccbb000*33 is too big to turn into a 32-bit int. In JS I think this is silently handled but adding a & 0xffffffff there helps it. Unfortunately, after that it seems that XOR is not supported:

[!] Symbolic execution does not support operand ^, concretizing.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ExpoSEJS/ExpoSE/issues/107#issuecomment-908500062, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABYJP3CUQXWTKBUSZSWJ4TT7OYE7ANCNFSM5DCE73EQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.