Is there a way to specify when a value should be declassified?

[bjohannesmeyer]

As an example, suppose we want to verify xor in xor.c:

#include <smack.h>
#include "../ct-verif.h"

void xor(int *key, int *out) {
  // key is secret, out is public
  *out = key[0];
  *out ^= key[1];
}

void xor_wrapper(int *key, int *out) {
  public_in(__SMACK_value(key));
  public_in(__SMACK_value(out));
  public_in(__SMACK_values(out,1));
  public_out(__SMACK_values(out,1));
  declassified_out(__SMACK_values(out,1));

  xor(key, out);
}

The xor function xors the two secret values in key and stores the result in the public out. It does this by erroneously storing the intermediate value in out, thereby leaking key[0]. However, ct-verif verifies this program with the following command in an examples subdirectory: WD=${PWD} ENTRYPOINTS=xor_wrapper EXAMPLE=xor.c make -C ../../bin verify.

Is this a problem? It seems like it would be since key[0] is leaked, but I may be doing something wrong.

[fdupress]

declassified_out annotations are trusted and are part of the model. By annotating the span of out as declassified_out, you are telling ct-verif to consider as leakage only differences in execution trace that cannot be explained by differences in the values stored in out.

Try removing the declassified_out annotation?

[Not sure the initial explanation made complete sense: I can clarify it as needed if I set aside a bit more time.]

[fdupress]

Sorry, I also missed some other details of your example.

Can you confirm that you are worried about intermediate values of out being observed by the adversary rather than the final value? If so, this is currently out of the family of models that could be covered by ct-verif. Something could probably be done (adding a monitored_out annotation that would add to the trace all values written to the monitored variable), but it seems like a problem better solved by (much) simpler methods.

[bjohannesmeyer]

Thanks for the response! I don't think I was clear in the example. key[0] and key[1] are secret here, but key[0]^key[1] is public. So yes, in this example I'm worried that the intermediate value of *out = key[0] will be leaked to the adversary.