Overview

HTTPS SSH
This archive contains the proof-of-concept implementation as well as all the 
input files to reproduce the experiments for the CAV'16 paper 'Synthesis of 
Fault-Attack Countermeasures for Cryptographic Circuits'. Instructions for 
reproducing the experiments can be found below.


Installing the tool:
====================
So far, this tool has been tested on Linux systems only. In order to 
make it run, you need to:
 - Extract the tar-ball to HOME directory of your computer
 - Make sure you have sygus enumerative solver installed(please do not download directly from offical website, we have some source code revised for our tool)
   More info on sygus can be found here: https://github.com/rishabhs/sygus-comp14 	
 - Add "yices" and sygus to user path:
   echo 'export PATH=$PATH: ~/FAC/yices-1.0.40/bin' >>~/.bashrc
   echo 'export PATH=$PATH:~/sygus/enumerative/esolver-synth-lib/bin/debug' >>~/.bashrc
 - Build LLVM using the commands
   cd ~/FAC/build
   ../bin/config_llvm3.sh
   make; make install 
 - if you have sygus and FAC folder in different location, please update
   FAC/llvm-3.0.src/tools/clang/lib/AST/StmtDumper.cpp on line 13556 and line 14404 to corresponding directory

Or you can download our virtual machine here: http://goo.gl/kpUIr7, with Username: cav and Password: ae.
It is in the OVF format, you are supposed to open it with any mainstream virtual machine software. 
For example, you can download Vmware Player for free here: https://goo.gl/FQAQEG

Running our synthesis tool:
===========================
 - Copy benchmark files from FAC/Benchmarks/Benchmarks_C/x-Px to FAC/cryptoSyn
 - Open a shell in FAC/build/Release+Debug+Asserts/bin
 - Run the tool by:
   time ./clang -cc1 -ast-dump ~/FAC/cryptoSyn/code.cpp

Reproducing the results from the paper:
=======================================
after execute the command: time ./clang -cc1 -ast-dump ~/FAC/cryptoSyn/code.cpp
You are expected to see:

Reading synSpec.txt

****** regionLim = 2
, time is Tue Jan 12 07:32:44 2016



++++++++ code before synthesis changes +++++++++++
int compute( arguments to be added){
N35  =  N34  ^  N10 ;
N34  =  N32  ^  N13 ;
N32  =  N31  ^  N33 ;
N31  =  N29  ^  N30 ;
N29  =  N8  ^  N27 ;
N8  =  N9  &  N5 ;
N9  =  r2 ;
N5  =  N6  ^  N7 ;
N6  =  k3 ;
N7  =  r3 ;
N27  =  N24  &  N28 ;
N24  =  N25  ^  N26 ;
N25  =  k2 ;
N26  =  r2 ;
N28  =  r3 ;
N30  =  N3  ^  N23 ;
N3  =  N1  &  N4 ;
N1  =  ~ N2 ;
N2  =  r2 ;
N4  =  r3 ;
N23  =  N19  &  N20 ;
N19  =  ~ N16 ;
N16  =  N17  ^  N18 ;
N17  =  k2 ;
N18  =  r2 ;
N20  =  N21  ^  N22 ;
N21  =  k3 ;
N22  =  r3 ;
N33  =  r4 ;
N13  =  N14  ^  N15 ;
N14  =  k1 ;
N15  =  r1 ;
N10  =  N11  ^  N12 ;
N11  =  r1 ;
N12  =  0 ;
int, N35, N34, N32, N31, N29, N8, N9, N5, N6, N7, N27, N24, N25, N26, N28, N30, N3, N1, N2, N4, N23, N19, N16, N17, N18, N20, N21, N22, N33, N13, N14, N15, N10, N11, N12;
return(N35);
}


== total buf alg node count is 51

Levels = 3

Gates:
and
or
not
xor

p3: Next sensitive node is 23
k2 root = 350.25user 0.12system 0:00.38elapsed 99%CPU (0avgtext+0avgdata 55824maxresident)k
0inputs+8outputs (0major+3573minor)pagefaults 0swaps

Synthesis iteration successful :)

+ Partial code AFTER synthesis changes +
//Solution 0:
n1  = n2 and n3 ;
n2 = LN19 ;
n3  = n4 and n4 ;
n4 = LN20 ;





get program from file and then update (regRoot = 23, node reach = 35)

++++++++ complete code after synthesis changes +++++++++++
int compute( arguments to be added){

 Removed for nowint;
return(N35);
}

press enter to continue
p3: Next sensitive node is 34
k2 root = 350.00user 0.04system 0:00.05elapsed 98%CPU (0avgtext+0avgdata 55824maxresident)k
0inputs+8outputs (0major+3580minor)pagefaults 0swaps

Synthesis iteration successful :)

+ Partial code AFTER synthesis changes +
//Solution 0:
n1  = n2 xor n3 ;
n2 = LN32 ;
n3  = n4 and n4 ;
n4 = LN13 ;





get program from file and then update (regRoot = 34, node reach = 36)

++++++++ complete code after synthesis changes +++++++++++
int compute( arguments to be added){

 Removed for nowint;
return(N35);
}

press enter to continue
p3: Next sensitive node is 34
k2 root = 350.00user 0.02system 0:00.03elapsed 97%CPU (0avgtext+0avgdata 56368maxresident)k
0inputs+8outputs (0major+3580minor)pagefaults 0swaps

Synthesis iteration successful :)

+ Partial code AFTER synthesis changes +
//Solution 0:
n1  = n2 xor n3 ;
n2 = LN32 ;
n3  = n4 and n4 ;
n4 = LN37 ;





get program from file and then update (regRoot = 34, node reach = 37)

++++++++ complete code after synthesis changes +++++++++++
int compute( arguments to be added){

 Removed for nowint;
return(N35);
}

press enter to continue
p3: Next sensitive node is 31
k2 root = 350.00user 0.05system 0:00.07elapsed 90%CPU (0avgtext+0avgdata 56224maxresident)k
0inputs+8outputs (0major+3580minor)pagefaults 0swaps

Synthesis iteration successful :)

+ Partial code AFTER synthesis changes +
//Solution 0:
n1  = n2 xor n3 ;
n2 = LN30 ;
n3  = n4 and n4 ;
n4 = LN29 ;





get program from file and then update (regRoot = 31, node reach = 38)

++++++++ complete code after synthesis changes +++++++++++
int compute( arguments to be added){

 Removed for nowint;
return(N35);
}

press enter to continue
p3: Next sensitive node is 34
k2 root = 350.00user 0.00system 0:00.01elapsed 100%CPU (0avgtext+0avgdata 56384maxresident)k
0inputs+8outputs (0major+3581minor)pagefaults 0swaps

Synthesis iteration successful :)

+ Partial code AFTER synthesis changes +
//Solution 0:
n1  = n2 xor n3 ;
n2 = LN32 ;
n3  = n4 and n4 ;
n4 = LN38 ;





get program from file and then update (regRoot = 34, node reach = 39)

++++++++ complete code after synthesis changes +++++++++++
int compute( arguments to be added){

 Removed for nowint;
return(N35);
}

press enter to continue
p3: Next sensitive node is 34
k2 root = 350.00user 0.00system 0:00.01elapsed 92%CPU (0avgtext+0avgdata 56384maxresident)k
0inputs+8outputs (0major+3581minor)pagefaults 0swaps

Synthesis iteration successful :)

+ Partial code AFTER synthesis changes +
//Solution 0:
n1  = n2 xor n3 ;
n2 = LN32 ;
n3  = n4 and n4 ;
n4 = LN40 ;





get program from file and then update (regRoot = 34, node reach = 40)

++++++++ complete code after synthesis changes +++++++++++
int compute( arguments to be added){

 Removed for nowint;
return(N35);
}

press enter to continue
p3: Next sensitive node is 34
k2 root = 350.00user 0.02system 0:00.03elapsed 97%CPU (0avgtext+0avgdata 56368maxresident)k
0inputs+8outputs (0major+3580minor)pagefaults 0swaps

Synthesis iteration successful :)

+ Partial code AFTER synthesis changes +
//Solution 0:
n1  = n2 xor n3 ;
n2 = LN32 ;
n3  = n4 and n4 ;
n4 = LN41 ;





get program from file and then update (regRoot = 34, node reach = 41)

++++++++ complete code after synthesis changes +++++++++++
int compute( arguments to be added){

 Removed for nowint;
return(N35);
}

press enter to continue
p3: Next sensitive node is -1
Finised, program secure now.

=-= total buf alg node count is 51
*************************************
*************************************
********* STATISTICS ****************
*************************************
* 1: Initial node count = 35
* 2: Buffer insertion algorithm final node count = 51
* 3: Buffer insertion algorithm percentage node increase compared to initial = 45.71%
* 4: Total iterations count (synthesis calls) = 7
* 5: Succesful iterations count = 7
* 6: Fail iterations count = 0
* 7: Final synthesis node count = 42
* 8: Synthesis percentage node increase compared to initial = 20%
* 9: Synthesis percentage nodes decrease compared to buffer insertion algorithm = 17.65%
*10: TotTime  = 100k 6e110w
*11: Average synthesis time  = 100k 6e110w


++++++++ Depth +++++++++++


 preDepth = 8

 postDepth = 8

+++++++++++++++++++

real	0m1.933s
user	0m1.332s
sys	0m0.564s



Any questions? Do not hesistate to contact the authors of the paper.

Have fun!