lac-dcc / lif Goto Github PK
View Code? Open in Web Editor NEWA tool to eliminate timing-based side channels
License: GNU General Public License v3.0
A tool to eliminate timing-based side channels
License: GNU General Public License v3.0
Currently, we deliver operation invariance to all programs, since PCFL removes all branches controlled by sensitive information. However, this might introduce non-termination into programs that originally were guaranteed to terminate. Consider the following examples:
int foo(int secret) {
while (use(secret)) {
// do something
}
}
After PCFL, the loop exit controlled by secret
will no longer exist. In this case, since there are no public exits, the loop will be disconnected from the rest of the CFG. This can be determined statically and reported back to the user.
int bar(int public, int secret) {
while (use(secret)) {
// do something
if (use(public)) break;
}
}
In this example, the loop exit controlled by secret
will be erased, by the other exit controlled by public
will still exist after PCFL. Furthermore, there might be values of public
such that use(public)
never evaluates to true, leading to an infinite loop. Unfortunately, it is not possible to determine statically whether the loop will terminate or not.
One alternative solution is to follow an approach similar to that of Constantine: come up with an upper bound for the loop, potentially reducing the information leaked but not necessarily eliminating the side-channel completely. Constantine runs a dynamic analysis to "guess" an initial value for the upper bound and then adds code to update it whenever breached during execution. Instead of running a dynamic analysis, we can rely on non-determinism to define such an upper bound:
int bar_pcfl(int public, int secret) {
int rlimit = random(k); // number from 0 to k, uniform distribution
while (true) {
// do something
if (use(public)) break;
// is_dummy is true when the loop should have exited
// dummy_n is the number of dummy iterations executed so far
if (is_dummy & dummy_n == rlimit) break;
}
}
Originally, for a particular instance p
of public
, each value s
of secret
were mapped to exactly one trace of instructions. To simplify, we can replace "trace of instructions" with "loop exits at the i-th iteration". To illustrate, consider that there are only three possible values s_i
of secret
and each s_i
causes the loop to exit at the i-th iteration. This can be represented as follows:
1 | 2 | 3 | |
---|---|---|---|
s_1 | 1 | 0 | 0 |
s_2 | 0 | 1 | 0 |
s_3 | 0 | 0 | 1 |
where rows are indexed by the secret (X) and columns by the last iteration of the loop (Y). Each cell represents the conditional probability p(x | y). We can quantify the amount of information leaked using Bayes vulnerability, which (assuming that the secrets are uniformly distributed) can be computed as the sum of the column maximums (see the "Science of Quantitative Information" book, multiplicative Bayes leakage, uniform prior):
1 + 1 + 1 = 3 (probability of guessing the secret right is 3x greater once the functions has been executed)
Now, consider that we choose a number from 0 to 2 (inclusive) as the upper limit for the dummy iterations of the loop (all numbers are equally likely to be picked). Then, when given s_1
as secret input the loop can terminate at the 1st, 2nd or 3rd iteration; when given s_2
, at the 2nd, 3rd or 4th iteration; and, when given s_3
, at the 3rd, 4th or 5th iteration. Notice that there are intersections between the possible last iterations. This can be represented as follows:
1 | 2 | 3 | 4 | 5 | |
---|---|---|---|---|---|
s_1 | 1/3 | 1/3 | 1/3 | 0 | 0 |
s_2 | 0 | 1/3 | 1/3 | 1/3 | 0 |
s_3 | 0 | 0 | 1/3 | 1/3 | 1/3 |
The multiplicative leakage is 5 * 1/3 = 1.67. Thus, the leakage after PCFL + upper limit was reduced, but not completely eliminated.
For side-channel verification, the taint analysis considers both data and control dependencies. However, by linearizing secret-dependent branches we remove control dependencies, so our taint analysis should consider only control dependencies that remain in the program after linearization (but we need the taint analysis in order to be able to linearize something, hence the "look-ahead" term).
Consider the following piece of code:
if (use(secret)) {
// do something
} else {
// do something else
}
// pdom
The predicate that controls the if statement is data dependent on a secret. Thus, that if statement will be linearized and any control dependency from the predicate to instructions inside the then or the else paths will be removed as long as the effects of such instructions don't escape the influence region of said predicate (i.e., they don't affect anything from pdom onwards). The question then is: when does something escape the influence region of a predicate?
To the best of my knowledge, there are only two scenarios to consider:
a) phi functions
if (use(secret)) {
x0 = 0
} else {
x1 = 1
}
x = phi x0, x1
if (use(x)) {
// do something
}
We already handle phi functions!
b) store + load
if (use(secret)) {
*x = 0
} else {
*x = 1
}
if (use(*x)) {
// do something
}
This is currently not implemented. There are benchmarks in our test suite that contain this pattern. One example is ghostrider/dijkstra. To circumvent this problem, we currently identify and mark variables as secret by hand. In the case of dijkstra
, we had to mark the vectors vis
and dis
as secret. This process is done as follows:
#define secret __attribute__((annotate("secret")))
secret int secret_var;
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.