Declassification

[real-or-random]

Can this extended to support declassification?

For some context, in secp256k1, we use valgrind for a runtime analysis for constant-timeness, and we implemented a declassify operation that uses some valgrind magic to allow some leakage, e.g., it's public if creating a digital signature was created successful, even though this depends on the secret key, see
https://github.com/bitcoin-core/secp256k1/blob/f39f99be0e6add959f534c03b93044cef066fe09/src/secp256k1.c#L502

[cdisselkoen]

Pitchfork supports declassification at the function-level via function hooks. Specifically, if you specify a hook for some function (say, a SHA-256 hash function), you can return whatever value you want from your hook, secret or not. This allows you to declassify the result of the hash function, even if the inputs were secret. You can also use function hooks to write public data to memory in places that formerly held secrets, thus marking those memory locations as public.

A direct declassify operation isn't possible in the current design of Pitchfork because secret values are "opaque", meaning that Pitchfork doesn't track the actual symbolic expression corresponding to secret variables. In general, opaque secrets save a lot of computation time because neither Pitchfork nor its SMT solver need to reason about the values of secret variables, and this is still perfectly safe because if a secret variable would be used for anything "important" to symbolic execution (such as in a memory address or branch condition), this would represent a constant-time violation anyways. Unfortunately though, this means that a given secret value can't just easily be turned public, because that would require knowing its value as a symbolic expression.

I've found the function-level declassification provided by Pitchfork to be sufficient for my own use cases, but I'd be curious if you have a use case where it doesn't work.

[real-or-random]

Thanks for the reply. This makes sense in general but do you have some example code? I think this would help me understand.

[cdisselkoen]

Suppose we have a function (in C) which processes secret data in arr and returns an int:

int my_function(int* arr) {
    // some computation which depends on the data in arr
}

Without a function hook, Pitchfork will end up returning a secret value from this function, because the return value is influenced by secrets. To declassify this value, we can use haybale::function_hooks::generic_stub_hook as a hook for this function, which will return a completely unconstrained public value. This also means that Pitchfork won't symbolically analyze the contents of my_function, due to the hook.

If we want Pitchfork to symbolically analyze the contents of my_function but then still return a public rather than secret value, one way would be to add a simple function call to the C source:

// before:
int my_function(int* arr) {
    // some computation which depends on the data in arr
    return retval;
}
// after:
int my_function(int* arr) {
    // some computation which depends on the data in arr
    return declassify(retval);
}

where declassify() has the following definition in C:

int declassify(int x) { return x; }

but we configure Pitchfork to use haybale::function_hooks::generic_stub_hook for declassify() so that it returns an unconstrained public value. Note that declassifying at the end like this still means that Pitchfork will have no knowledge of the actual symbolic expression that should be returned - the return value will be completely unconstrained, meaning Pitchfork will consider any value as a possible return value from my_function. If this is not desired, we would have to declassify earlier in my_function, or perhaps declassify the output of some function which my_function calls.

[elichai]

Thanks! could you maybe show an example of how that looks like?
I currently have this PoC, that complains to me about a return value that should be declassified, just like in your example
I'm not sure how the generic_stub_hook is supposed to connect to the project and check_for_ct_violation
https://gist.github.com/elichai/a28dedd9dae95486a405dc6aa08db7ab

[cdisselkoen]

Config.function_hooks will allow you to specify generic_stub_hook for any function you choose.

config.function_hooks.add("some_function_name", &generic_stub_hook);

Or is that not the question?

[elichai]

Or is that not the question?

Yeah, that was the question, but creating the needed parameters for the stub hook isn't easy either :)
I can create a State like that:

    let noncefp = project.get_func_by_name("secp256k1_nonce_function_default").unwrap();
    let location = Location {
        module: noncefp.1,
        module: noncefp.0,
        bb: &noncefp.0.basic_blocks[0],
        instr: BBInstrIndex::Instr(0),
        source_loc: None,
    };
    let mut state = State::new(&project, location, config);

Which I hope is correct? but creating a &dyn IsCall is harder, I need either a Call or Invoke and I can't figure out how to get/create those

[cdisselkoen]

You don't need to create parameters for the stub hook - you just pass the function hook into the Config as I showed above, and you should be good to go. Pitchfork will call the hook as needed.

[elichai]

Should've checked the signature of add before checking the stubs signature lol, thanks!

[unseddd]

You don't need to create parameters for the stub hook - you just pass the function hook into the Config as I showed above, and you should be good to go. Pitchfork will call the hook as needed.

Is there a way to call into a function defined by an external C library? Understand that function hooks can be used to elide calls to library functions, but would like to actually be able to call into a function (e.g. secp256k1_ecdsa_sign).

[unseddd]

@cdisselkoen also getting the following error when trying to add a function hook with generic_stub_hook:

config.function_hooks.add("secp256k1_ecdsa_sign", &generic_stub_hook);
                                                  ^^^^^^^^^^^^^^^^^^

                                                  expected signature of `for<'r> fn(&tests::pitchfork::Project, &'r mut haybale::state::State<'_, _>, &dyn haybale::function_hooks::IsCall) -> _`
                                                  found signature of `for<'r, 's, 't0, 't1> fn(&'r tests::haybale::Project, &'s mut tests::haybale::State<'t0, _>, &'t1 (dyn tests::haybale::function_hooks::IsCall + 't1)) -> _`

Code snippet:

extern crate haybale;
extern crate pitchfork;

use pitchfork::{
    AbstractData,
    Config,
    PitchforkConfig,
    Project,
    StructDescriptions,
    check_for_ct_violation,
};

use haybale::function_hooks::generic_stub_hook;

...

let mut config = Config::default();
config.loop_bound = 100;
config.function_hooks.add("secp256k1_ecdsa_sign", &generic_stub_hook);

Am I doing something obviously wrong here?

[cdisselkoen]

Is there a way to call into a function defined by an external C library? [not using a hook, but actually analyzing the function]

Sure! Just compile the external library to bitcode and add those bitcode files to your Project. (See the documentation on Project for several options for doing this.) It should be as easy as that.

also getting the following error ...

It looks like there's a confusion between haybale::Project and pitchfork::Project (Pitchfork re-exports haybale's Project type). This might be fixable by using haybale::Project in your code instead of pitchfork::Project. Perhaps the re-export was a mistake - I was expecting the types to be interchangeable but it appears they are not.

[unseddd]

Perhaps the re-export was a mistake - I was expecting the types to be interchangeable but it appears they are not.

Tried with haybale::Config and haybale::Project, but that causes separate type issues. Think the re-export is necessary, and maybe re-exporting generic_stub_hook is a good idea as well. Will tinker and report back.

[cdisselkoen]

Actually - Pitchfork does export some function hooks itself: see these docs. The return_public_unconstrained hook should work instead of generic_stub_hook in this case, avoiding the issue.

[unseddd]

Ok, can confirm that re-exporting generic_stub_hook also works, if the more general solution is needed.