\documentclass{llncs-rabbi}


\usepackage{url}
%\usepackage{graphics}
\usepackage{amssymb}
\usepackage{amsmath}
%\usepackage{amsthm}
\usepackage{subfigure}
\usepackage{epsfig}

% Add \contrib{} from /usr/local/teTeX/share/texmf.tetex/amslatex/tex/latex/amscls/amsproc.cls

\newcommand\V[1]{\overrightarrow{#1}}
%\theoremstyle{plain}		\newtheorem{definition}{Definition}
%\theoremstyle{plain}		\newtheorem{observation}{Observation}
%\theoremstyle{plain}		\newtheorem{theorem}{Theorem}
%\theoremstyle{plain}		\newtheorem{lemma}{Lemma}


% Cut down on whitespace above and below figures displayed at head/foot of
% page.
\setlength{\textfloatsep}{3mm}
% Cut down on whitespace above and below figures displayed in middle of page
\setlength{\intextsep}{3mm}


\setcounter{page}{1}

\begin{document}

\title{Guns and Butter: Toward Formal Axioms of Input Validation}

\author{Meredith L. Patterson\inst{1} and Robert J. Hansen\inst{1} and Len Sassaman\inst{2}}

\institute{The University of Iowa Department of Computer Science\\
Iowa City, Iowa, 52242 USA
\email{\{mlpatter,rjhansen\}@cs.uiowa.edu}
\and
K. U. Leuven ESAT-COSIC \\
Kasteelpark Arenberg 10, B-3001 Leuven-Heverlee, Belgium
\email{len.sassaman@esat.kuleuven.be}
}


\maketitle
%\pagestyle{empty}
%\centerline{\LARGE\bf DRAFT --- not for publication}
%======================================================================

\begin{abstract}

Input validation has long been recognized as an essential part of a well-designed system, especially when considering defense against an external adversary, yet existing literature gives little in the way of formal axioms for input validation or guidance on putting into practice what few recommendations exist~\cite{FIXME}. 

In the domain of network security, the problem of input validation is often avoided by maintaining strict control over the network's perimeter or sensitive systems, and restricting input from untrusted users. However, in cases where a service exists to provide content to untrusted users in response to their requests, this type of protection is infeasible. Such is the case with many dynamically-generated websites or databanks that allow untrusted users to submit \textsc{sql} queries to a database. We examine existing solutions to a common network threat, the \emph{\textsc{sql} injection attack}, and agree with existing literature~\cite{FIXME} that input validation is critical in addressing this attack.

We then present basic formal axioms for input validation, and apply them to \textsc{sql}, where we demonstrate enhanced resistance to injection attacks against databases using our input validation library.

\end{abstract}


\section{Introduction}
 
\textsc{sql} injection attacks have been a leading method of network compromise since their discovery in XXXX~\cite{}. Blah blah blah. Numerous methods have been proposed and deployed to hinder or inhibit injection attacks on \textsc{sql}, to varying success. In this paper, we review the techniques both proposed in the literature, and deployed in the field. There is agreement in the literature that strong input validation is the proper approach to solving injection attacks in general.~\cite{FIXME}. However, the literature is lacking both in a set of formal axioms for input validation, as well as guidance for the implementors of systems concerned with input validation. We present such a framework in Section \ref{framework}, say something else in Section \ref{}, and show our approach as applied to \textsc{sql} in Section \ref{}. In Section \ref{dejector}, we discuss {\tt Libdejector}, our approach as implemented as a PostgreSQL~\cite{} library.
 
\section{Injection attacks}

Talk about injection attacks, esp

\subsection{\textsc{sql} Injection}
\subsubsection{regex, etc...}

\section{The need for formal models} 

(This could be the place where we introduce the notion of language-theoretic security, i.e., limiting the user's capabilities by limiting the expressive power of the language and limiting the expressive power of the language by limiting both the complexity of its syntax and the semantic content captured in the vocabulary. I'm sure we can dig up plenty of examples of people doing things which ought not be done, just using the tools available to them -- simple ones like Towers of Hanoi in sendmail rules pave the way for more serious exploits.

As I see it, this section exists to motivate section 4 below, and gives us the formal-language street cred for this Sydney conference. I would like, if at all possible, to run it by what's-his-name from your office that does the formal security work, though.)
 
\section{Framework}
\label{framework}
\subsection{Definitions and Observations}
We begin with several definitions from elementary computability theory, and draw observations which motivate our work.

\begin{definition}[Validity]
A string S in a language L is valid if and only if S can be generated from the formal description of L.
\end{definition}

\begin{definition}[P-language]
A language L is a P-language if and only if all strings generated by L exhibit the property P.
\end{definition}

\begin{observation}[Validity of sublanguages]
All strings in the P-language L' derived from L are valid P-strings in L, regardless of whether L is a P-language.
\end{observation}

This observation, while quite general, has practical consequences. 
By constructing a properly constrained sublanguage of an insecure language, we may generate secure strings within that insecure language.

\begin{definition}[M-set]
The M-set of languages is composed of all languages which require a mechanism of minimum strength M for their generation.
\end{definition}

\begin{definition}[Syntactic context]
\label{def:syntactic-context}
The syntactic context for an input I in a string S is the maximum extent in S to which I can change the syntactic structure (or \emph{parse}) of S, up to an upper bound of the entirety of S.
\end{definition}

We denote the syntactic context of $S$ for a given input $I$ with the notation $\Sigma_I^S$. 
When a string refers to a variable, we note that for any variable $V$ defined in a syntactic context $\Sigma^T$, any syntactic context $\Sigma^S$ which references $V$ will incorporate $\Sigma^T$.

\begin{definition}[Semantic context]
A semantic context for an input I in a string S is the maximum extent to which I can change the semantic meaning of S, up to an upper bound of the entirety of S.
\end{definition}

We denote the semantic context of $S$ for a given input $I$ with the notation $\Upsilon_I^S$. 
Our discussion of $\Upsilon_I^S$ will be limited, as semantic analysis is beyond the scope of this paper except insofar as it can be facilitated via syntactic analysis.

\subsection{Input Validation Theorems}
\begin{theorem}[Minimum validation strength]
\label{th:minval}
Given a language L which requires a minimally--strong computational mechanism M to generate strings $\in$ L, an arbitrary string S $\in$ L must be validated using a mechanism at least as strong as M.
\end{theorem}
\emph{Proof.} Since validating a string against a language is done by applying the production rules of the language to create the string being validated, if it is possible to validate $S$ using a mechanism weaker than $M$, then $M$ is not the minimally--strong mechanism required to generate $L$'s productions. 
This contradicts our statement that $M$ is minimally strong.

Note that it is trivial to generate a one-off instance of a computational mechanism weaker than $M$ which validates one or more strings in $L$, but this does not invalidate this theorem.
Consider $L = \{all strings of the form a^nb^n\}$.
This language is context-free, but a finite state machine $F$ can be constructed which validates strings in $L$ of some finite length $l$.
However, $L$ still contains an infinite number of strings which $F$ cannot validate; validating an arbitrary string in $L$ requires a context-free grammar.

\begin{observation}[Maximal validation strength]
A language L requiring a minimally--strong computational mechamism M should not be validated using a mechanism stronger than M.
\end{observation}

Hoglund and McGraw\cite{hoglund-mcgraw} note that ``a complex computational system is an engine for executing malicious computer programs delivered in the form of crafted input.''
Their concern --- the inevitable compromise, given enough time, of systems --- informs this observation.
If we assume that systems will be compromised at some point, prudence requires that we expose to our attackers the weakest mechanism possible.
An attacker given access to a strong mechanism has far more potential for mayhem than one using a weaker mechanism.

\begin{theorem}[Range of validation]
\label{th:rangeval}
Given an input I and a string S, validation must occur over at least the range $\Sigma_I^S$.
\end{theorem}
\emph{Proof.} Since $\Sigma_I^S$ is defined as the greatest extent to which $I$ has the capability to influence the parse of $S$, validating a range smaller than $\Sigma_I^S$ may result in failure to validate all the syntactic changes $I$ may introduce to $S$.
Validation of only $I$ is sufficient in only those cases where it can be proven $\Sigma_I^S = I$.

\begin{lemma}[Construction of sublanguages]
\label{lem:sublanguage-construction}
Given context-free grammars G and H, where $H = \langle V, T, R, S \in V \rangle$, L(G) is a sublanguage of L(H) if $V(G) \subseteq V(H), T(G) \subseteq T(H), R(G) \subseteq R(H)$ and $S(G) = S(H)$.
\end{lemma}
\emph{Proof by Construction.} For any string $w$ in $L(G)$, there exists a production $P(w) \in G$.
All variables, terminals, and rules used in $P(w)$ are correspondingly in $G$. $S(P(w)) = S(G)$.
$V(P(w))$ must necessarily exist in $V(G)$, which as a given exists in $V(H)$. 
Similar arguments exist for $T, R, S$. 
Thus, $P(w) \in H$ and $w \in L(H)$.
Consequently, since any arbitrary string in $L(G)$ is also a string in $L(H)$, $L(G)$ is a sublanguage of $L(H)$.

\begin{observation}[Mechanism equivalence]
\label{obs:equiv}
Any regular expression, finite-state automata or pushdown automata can be converted into an equivalent context-free grammar, and thus falls under Lemma \ref{lem:sublanguage-construction}.
\end{observation}

\subsection{Injection Formally Defined}

In practice, attackers use injection to retrieve information which they cannot access legitimately or to manipulate the state of some set of information (e.g., unauthorized \textsc{insert} or \textsc{delete} queries on a relational database).
Either the contents of the result set or the contents of the information set will differ from those which a non-injected query would produce.
This necessarily alters both the semantic meaning and the syntactic structure of the query string.

However, altering syntactic structure need not change semantic meaning.
Adding any number of repetitions of the clause {\tt and '1' =  '1'} to the {\sc where} clause of an \textsc{sql} {\textsc{select} statement will not produce a change in the contents of the result set, because $\forall P$, $P \wedge True \rightarrow P$ by identity.
Each repetition changes the parse, though, and a sufficiently large number of repetitions could produce observable effects in the state of the machine responding to the query (e.g., increased \textsc{cpu} or memory consumption during query processing, since systems which parse user input typically transform the entire parse tree into an in-memory representation and do not resolve tautologies or identities\footnote{Indeed, identifying all tautologies and identities is impossible in practice.
While string-literal comparisons are easily identified, given minimal knowledge of a database schema an attacker can still compose comparisons of variable data which always evaluate to $True$, e.g. {\tt user.id = user.id} or {\tt count(id) > -1}.}).
As unnecessarily increased resource consumption is also harmful, we argue that query alteration which alters syntactic structure but not semantic meaning constitutes injection as well.

Thus, consider a string $S$ containing a variable $V$ for which some input string $I$ (of fixed or variable length) is substituted, and for which a unique parse $P(S)$ is expected.

\begin{definition}[Injection input]
\label{def:injection}
Any $I$ which, when substituted for $V \in S$, results in a successful parse $P'(S) \neq P(S)$ constitutes an injection input.
\end{definition}

\section{Axiomatic Input Validation}
The conventional wisdom for validating user inputs is to use regular expressions to filter out bad inputs or allow in only good ones. 
A schism exists over which is the safest way to perform regular expression validation: whether it is better  to identify and allow through only those inputs known to be good, or to to identify and forbid inputs known to be bad~\cite{XXXXFIXME}.
However, this misses the more important point: for a majority of input situations, regular expressions are computationally insufficient for input validation.
As Theorem \ref{th:minval} shows, attempts to validate $\Sigma_I^S$ using a mechanism weaker than $M$ will often fail to recognize valid strings or identify invalid ones.

\subsection{Guns or Butter}
%rewrite this to be clearer, and avoid unsubstantiated statements.
It is not possible to create a regular expression which will reliably match $a^mb^m$, a language which is well-known to be context-free.
Any finite state machine designed to recognize this language will either accept some string $a^mb^n$, $m \neq n$ (the \emph{pigeonhole principle}), or reject a sufficiently long $a^mb^m$.
Attempting to coerce regular expressions into handling this language will inevitably lead to friction between what the regular expression can do, what developers think it can do, and what users need it to do.
In practice, developers end up erring on either the side of safety or the side of convenience.
Those who favour the former argue that we must admit only those inputs which a regular expression can verify as valid, and accept the false-positive rate (and its attendant inconvenience) as a necessary expense of security.
Those who prefer the latter say we must exclude only those inputs known to be bad, and accept the false-negative rate (and the security holes opened up) as a necessary expense of convenience.
However, we assert that whether an error is made on the side of safety or the side of convenience, it remains an error.

\subsection{Guns and Butter}
% Where do we define a context-free grammar?
Shifting to a more appropriate tool --- in our $a^mb^m$ example, a context free grammar --- enables us to validate inputs as good or bad with perfect accuracy. 
No longer do we have to make the tradeoff between security and convenience; we can have both guns and butter. 
Although the input language may provide a means for malicious behaviour, it is possible to create subsets of the input language in which it is only possible to generate secure strings.
Lemma \ref{lem:sublanguage-construction} provides a mechanism for generating subsets of context-free languages and Observation \ref{obs:equiv} allows us to extend the lemma to regular languages and finite-state automata.

\section{Applying Axioms to {\sc Sql}}
\label{sql}
The Structured Query Language, \textsc{sql}, is an \textsc{ansi/iso} standard language for interacting with relational databases. 
User input is in the form of a string in some encoding, typically \textsc{ascii} or Unicode; the string is parsed by a context-free grammar, usually one generated by a parser generator such as {\tt yacc} or {\tt bison}.

\textsc{Sql} offers tremendous flexibility, but this flexibility can be used against implementors as easily as implementors can use it against its problem domain. 
In this section, we show how formal axioms of input validation give improved resistance to a certain class of attacks.

\subsection{\textsc{Sql} Injection}
\textsc{Sql} \emph{injection} is a class of attacks against software which interfaces with a database. 
An innocuous-looking statement, such as {\tt "select rights from table where username =} $I_1$ {\tt and password =} $I_2${\tt "}, can be subverted with carefully-chosen $I_n$ values.

For instance, if $I_1$ is {\tt "root"} and $I_2$ is the string {\tt "' or '1' = '1'"}, the final statement passed to the database is {\tt "select rights from table where username = 'root' and password = '' or '1' = '1'"}. 
This malformed boolean expression evaluates to true, so root's rights will be granted.
%Are the quotes right above? FIXME

There are two possible regular-expression-based solutions to this problem: disallow certain characters from user input, or accept only certain patterns.
(A third approach, \emph{prepared statements}, is similar to the second solution, but only applies to \textsc{sql} and cannot be extended to other injection vectors such as XML/XPath injection.
We will discuss this further shortly.)
Most developers take the first approach, examining input strings for control characters such as {\tt "}, which terminates a string argument prematurely and allows an attacker to inject a malicious boolean substring; {\tt ;}, which terminates a query and allows an attacker to inject additional queries in the same input string; or {\tt --}, which is used to comment out the remainder of a line and bypass any remaining portion of the intended input which would constitute an unparseable fragment.
The validator either rejects such strings or ``escapes'' those characters so that the database parser does not interpret them as control characters.
In the second approach, a regular expression such as {\tt [a-zA-Z0-9]+} is assumed to cover all possible valid inputs.
However, both approaches can reject valid inputs, and international encodings present problems which are far too unwieldy for regular expressions to handle in a reasonable fashion.

%(FIXME: expand on this here and reference the recent injection issue from {\tt http://www.postgresql.org/docs/techdocs.50})

Having shown that regular expressions are inadequate to the task, we return to Theorems \ref{th:minval} and \ref{th:rangeval}, which say we need to validate over $\Sigma_I^S$ using a mechanism at least as strong as that used to generate valid command strings --- in this case, a context-free grammar.

We do not know what the user will input, and as such, predicting $\Sigma_I^S$ is problematic. 
However, by Definition \ref{def:syntactic-context}, the upper bound of $\Sigma^S$ is the whole of $S$, so we elect to validate over the entire string.
(In practice, this is entirely computationally feasible, since $S$ must be parsed by the \textsc{sql} parser eventually anyway.)

So far, we have not validated anything. 
If we were to put the injected \textsc{sql} string through an \textsc{sql} parser, it would parse correctly.
The string is syntactically valid, but it is semantically invalid, in that it does not achieve the intended results.
Our challenge is to define a sublanguage of \textsc{sql} which only generates strings that have our intended semantic meaning --- ``safe'' strings, in other words.

Fortunately, defining a safe subset of \textsc{sql} for this case is simple. 
We define, using Lemma \ref{lem:sublanguage-construction}, a sublanguage of \textsc{sql} wherein the only allowed production rules are those which generate the sequence {\tt "select rights from table where username='{\sc terminal-string}' and password='{\sc terminal-string}'"}, where {\sc terminal-string} denotes a sequence of characters which derives no keyword or other syntactic structure. (FIXME: this is a shitty way of phrasing that.)

We take whatever command string $C$ we create from splicing together our command string and the user input, then determine whether $C$ is a valid string in our known-safe sublanguage, using a tool of sufficient computational strength to produce all valid strings in that sublanguage.
In this case, since we know that a context-free grammar is sufficient to generate \textsc{sql} strings and our known-good context-free sublanguage generates a subset of all possible valid \textsc{sql} strings, we know that a context-free grammar is sufficient for our purposes.
If $C$ is a valid string in our sublanguage, the input is good.
If it is not, the input is bad.

By so doing, we are secure against \textsc{sql} injection attacks.

\section{Dejector}
\label{dejector}

\section{Conclusions and future work}
\label{conclusions}

\subsection*{Acknowledgments}


\end{document}
 
 