smackers
Problem with __SMACK_value() in C++
In C, a function may be declared without explicitly giving the number of parameters, as explained in this stackexchange article
C++ does not support this C-style functions with unspecified number of arguments.
smack.h uses this C-style declaration for __SMACK_value, which poses a problem for verifying C++ code with Smack.
While we are at it, it would be good to also add a regression with __SMACK_value.
Regression test (test.cpp)
extern "C" {
#include <smack.h>
}
int main()
{
int x = 10;
__SMACK_value(x);
return 0;
}
compiling with
clang++-3.9 -std=c++14 -c -emit-llvm -o test.bc test.cpp
gives
regression.cpp:8:2: error: no matching function for call to '__SMACK_value'
__SMACK_value(x);
^~~~~~~~~~~~~
smack.h:34:15: note: candidate function not viable: requires 0 arguments, but 1 was provided
smack_value_t __SMACK_value();
^
1 error generated.
In C++, one typically uses a template-function for taking an argument of arbitrary type
template<typename T>
void __SMACK_value(T x); // accepts 1 arg of arbitrary type
Not sure though if templates work well for Smack's use case, i.e., to merely label the variable x in LLVM's IR
It seems, based on SmackRep::valueAnnotation, that __SMACK_value() can be used with only one or two arguments. Can we just make proper declarations for these two cases?
I think in the long run we should split SMACK headers into C and C++ specific ones, with maybe a top-level shared header.
As a workaround, I've had success with the following 'hack':
extern "C" {
//...
#ifdef __cplusplus
smack_value_t __SMACK_value(unsigned int*, ...);
#else
smack_value_t __SMACK_value();
#endif
//...
} // end of extern "C"
i.e., by declaring __SMACK_value for C++ as a variadic function (with C linkage to prevent name mangling).
The benefit of this declaration is that clang++ produces LLVM IR code for this variadic function that closely resembles the IR code that clang produces for the __SMACK_value() function. Hence, smack can parse the IR code; no changes toSmackRep.cpp are necessary.
With this hack, I have successfully tested a C++ variant of ct-verif's Tiny Encryption Algorithm example (see post below for details).
The problem with this workaround is that the type that __SMACK_value takes is now hard-coded into the declaration, in other words, it currently only works for unsigned int* (which I happened to need for the Tiny Encryption Algorithm example).
One idea to circumvent this problem would be to declare __SMACK_value as follows:
smack_value_t __SMACK_value(int, ...);
where int is a dummy parameter, which is needed only because variadic functions need at least one named parameter. Then smack would need to be updated (probably by altering SmackRep.cpp) such that it always ignores the first parameter to __SMACK_value; the second parameter would be the actual value, which can then be of any type. One would then use it as
__SMACK_value(0, v);
where 0 is the dummy int, and the actual value is the parameter v.
I have tried to implement this, currently without succes (my change seemed to break the ct-verif toolchain: bam ran into an error while processing smack's output).
FYI, my C++ variant of ct-verif's Tiny Encryption Algorithm C++ example is as follows:
(note that ct-verif uses smack internally)
invoking ct-verif
The entry point should now be the C++-mangled name (which is in my case _Z15encrypt_wrapperPjS_)
ct-verif.rb -e _Z15encrypt_wrapperPjS_ tea.cpp
filename: tea.cpp
Note that C++ language mode is determined from the.cpp extension
/* From https://en.wikipedia.org/wiki/Tiny_Encryption_Algorithm */
extern "C" {
#include "ct-verif.h" // is a C header
}
#include <stdint.h>
void encrypt (uint32_t* v, uint32_t* k) {
uint32_t v0=v[0], v1=v[1], sum=0, i; /* set up */
uint32_t delta=0x9e3779b9; /* a key schedule constant */
uint32_t k0=k[0], k1=k[1], k2=k[2], k3=k[3]; /* cache key */
/* Code */
for (i=0; i < 32; i++) { /* basic cycle start */
sum += delta;
v0 += ((v1<<4) + k0) ^ (v1 + sum) ^ ((v1>>5) + k1);
v1 += ((v0<<4) + k2) ^ (v0 + sum) ^ ((v0>>5) + k3);
} /* end cycle */
v[0]=v0; v[1]=v1;
}
void decrypt (uint32_t* v, uint32_t* k) {
uint32_t v0=v[0], v1=v[1], sum=0xC6EF3720, i; /* set up */
uint32_t delta=0x9e3779b9; /* a key schedule constant */
uint32_t k0=k[0], k1=k[1], k2=k[2], k3=k[3]; /* cache key */
/* Code */
for (i=0; i<32; i++) { /* basic cycle start */
v1 -= ((v0<<4) + k2) ^ (v0 + sum) ^ ((v0>>5) + k3);
v0 -= ((v1<<4) + k0) ^ (v1 + sum) ^ ((v1>>5) + k1);
sum -= delta;
} /* end cycle */
v[0]=v0; v[1]=v1;
}
void encrypt_wrapper (uint32_t* v, uint32_t* k) {
/* Boilerplate */
public_in(__SMACK_value(v));
public_in(__SMACK_value(k));
/* Useful */
// declassified_out_object(__SMACK_object(v,2 * sizeof(*v)));
encrypt(v,k);
}
void decrypt_cpa_wrapper (uint32_t* v, uint32_t* k) {
/* Boilerplate */
public_in(__SMACK_value(v));
public_in(__SMACK_value(k));
/* Useful */
public_in(__SMACK_values(v,2));
decrypt(v,k);
}
void decrypt_cca_wrapper (uint32_t* v, uint32_t* k) {
/* Boilerplate */
public_in(__SMACK_value(v));
public_in(__SMACK_value(k));
/* Useful */
public_in(__SMACK_values(v,2));
// declassified_out_object(__SMACK_object(v,2 * sizeof(*v)));
decrypt(v,k);
}
FYI, I've forked the ct-verif repo and created a Dockerfile for building a ct-verif environment (including the __SMACK_value work-around for Smack) that can verify the above C++ example. See:
https://github.com/niekbouman/verifying-constant-time/tree/cplusplus
My commits related to SMACK can be found here (in the variadic branch)
https://github.com/niekbouman/smack/tree/variadic
(the commits in the bouman branch are obsolete)
Excellent. I think the jury is still out on the right interface for __SMACK_value or something similar, but we will keep an eye on this. Your ideas are welcome!
