Security bugs

New titles?

• Unvalidated Input detection.
• Unvalidated user input detection

In this section we will define “security bugs” in the context of error traces. We want to answer the following 3 questions

• What is a security bug ? How can we formally define a security bug ?
• Given an error trace or a set of error traces, how can we find out if there is a security bug in the program ?
• How can we find out which statement is the cause of the security bug ?

Introduction

A security bug is a class of bugs in which a user input can directly influence whether we reach the error state or not. If we try to define this requirement a bit more formally, a bug is called a security bug if in an error trace, following three properties are satisfied:

1. There is some statement \( \mathbf{st} \) in the error trace where the program reads a user input.
2. There is some input value such that continuing the execution of the trace from \( \mathbf{st} \), we definitely reach the error.
3. There is some input value such that continuing the execution of the trace from \( \mathbf{st} \), we do not reach the error.

Examples

Consider the following example which demonstrates a simple case of buffer overflow caused by a user input:

/* Simple buffer overflow
 * Security
 * 
 * Author: Numair Mansur (mansurm@informatik.uni-freiburg.de)
 * Date: 2017-10-30
 */

int get_location(void);
int get_value(void);
int f(void);

void main(void) {
	int age[10];
	int location,value;
	location = get_location(); // from user
	value = get_value(); // from user
	age[location] = value;
}

In the above error trace, all three properties of a security bug are satisfied.

Now consider the following non-security case of the above example:

/* Simple buffer overflow
 * Non-Security
 * 
 * Author: Numair Mansur (mansurm@informatik.uni-freiburg.de)
 * Date: 2017-10-30
 */

int get_location(void);
int get_value(void);
int f(void);

void main(void) {
	int age[10];
	int location,value, r;
	location = get_location(); // from user
	value = get_value(); // from user
	r = f();
	if(r){
		age[location] = value;
	}
}

The program now has a variable r which is taking it’s value from an unknown function f(). This violates property 2 from our definition above and hence we will conclude that there is no security bug in this program.
To see more examples and to find out how we can find security bugs through Ultimate, click here.

Formal Definition

Execution: Let $\pi$ be an error trace of length $n$. An execution of $\pi$ is a sequence of states $s_0, s_1....s_n$ such that $(s_i, s_{i+1}) \models T$ where $T$ is the transition formula of $\pi[i]$.

Blocking Execution: An execution of a trace $\pi$ of size $n$ is called a blocking execution if there exists a sequence of states $s_0, s_1,..., s_j$ where $i<j \leq n$ such that $(s_i, s_{i+1}) \models T[i]$, where $T[i]$ is the transition formula of $\pi[i]$ and there exists an assume statement in the trace $\pi$ at position $j$ such that $s_{j} \not \Rightarrow guard(\pi[j])$.

Security bug: Let $\pi = \langle st_1,....,st_n \rangle$ be an error trace of length $n$ where $st_i$ is an assigning statement at position $i$ that assigns a value taken from a user to some variable $x$. The program contains a security bug if there exists an execution $s_1,...,s_{n+1}$ of $\pi$ and some values $v$ and $w$ such that if we start in the state $s_i$, every execution of the trace $\langle x:=v; \pi[i+1,n] \rangle$ is blocking and conversely no execution is blocking for the trace $\langle x:=w; \pi[i+1,n] \rangle$.

Algorithm:

From the formal definition above, and from the definitions of simple bug and definite bug, it is obvious that a program has a security bug if in a feasible error trace, an assigning statement which is taking it’s value from a user is relevant with respect to a simple bug and a definite bug. However, calculating the relevance of a statement for both simple and definite bug can be expensive and inefficient. We therefore propose the following alternative definition for security bug and prove that both definitions are equivalent.

Theorem: Let $\pi = \langle st_1,....,st_n \rangle$ be a feasible error trace of length $n$ and $\pi[i]$ be a havoc statement of the form $havoc(x)$ at position $i$ that assigns a non-deterministic value to the variabble $x$. The statement $\pi[i]$ is relevant with respect to both simple and definite bug iff it is the last error admitting statement in the trace.
Proof:
$" \Rightarrow "$
Let $\pi[j]$ be a havoc statement of the form $havoc(y)$ which assigns a non-deterministic value to the variable $y$ at position $j$ where $j > i$. Lets assume $\pi[j]$ is an error admitting statement. By definition, this will imply that there exits a value $v$ such that all executions of the trace $\langle x:=v; \pi[j+1,n] \rangle$ are blocking. Since we know that $\pi[i]$ is relevant with respect to definite bug, that means that for a value $w$, no blocking execution exists for the trace $\langle x:=w; \pi[i+1,n] \rangle$, which contradicts with our assumption that $\pi[j]$ is error admitting.
$" \Leftarrow "$
Let $\pi[i]$ be a havoc statement of the form $havoc(x)$ which assigns a non-deterministic value to the variable $x$ at position $i$. Since $\pi$ is a feasible error trace, we know that there exists an execution $s_1,...,s_{n+1}$ and some value $w$, such that if we assign $w$ to $x$, the trace $\langle x:=w; \pi[i+1,n] \rangle$ starting in the state $s_i$ has a non-blocking execution. Furthermore, since the statement is the last error admitting statement, no havoc exists after the position $i$ which is relevant with respect to a simple bug. This means that no execution of the trace $\langle x:=w; \pi[i+1,n] \rangle$ will be blocking. Hence $\pi[i]$ is relevant with respect to a definite bug.

Thanks to the modified definition, we can use our algorithm to find relevant statements with respect to simple bugs and efficiently find if there is a security bug in the program.

Algorithm 1. security($\pi$): Finding the presence of security bug in a program
———————————————————————————————————
  Input: error trace $\pi$ of length $n$
  Output: boolean value indicating the presence of a security bug
1   trace $\leftarrow$ error trace $\pi$
2   relevantPositions $\leftarrow$ relevance(trace)
3   for ( $i$ =relevantPositions.length() - 1 to $i$=0 )
4     if trace[ relevantPositions[$i$] ] is a user input then
5       return $true$
6   return $false$

Evaluation

[more to follow…]