96 lines
3.5 KiB
TeX
96 lines
3.5 KiB
TeX
\begin{schemeregion}
|
|
|
|
\section{An Extended Example}
|
|
|
|
To demonstrate the utility of refinement types as provided by Typed
|
|
Scheme,
|
|
we present an extended example, tackling the problem of form
|
|
validation. One important problem in form validation is avoiding SQL
|
|
injection attacks, where a piece of user input is allowed to contain
|
|
an SQL statement, and passed directly to the database. A simple is
|
|
example is the query
|
|
|
|
\begin{schemedisplay}
|
|
(string-append "SELECT * FROM users WHERE name = '" user-name "';")
|
|
\end{schemedisplay}
|
|
\noindent
|
|
If \scheme|user-name| is taken directly from user input, then it might
|
|
contain the string \scheme|"a' or 't'='t"|, resulting in an query that
|
|
returns the entire contents of the \verb|users| table. More damaging
|
|
queries can be constructed, with data loss a significant
|
|
possibility~\cite{xkcd}.
|
|
|
|
One common solution for avoiding this problem is sanitizing user input
|
|
with escape characters. Unfortunately, sanitized input, like
|
|
unsanitized input, is simply a string. Therefore, we use
|
|
refinement types to statically verify that only validated input
|
|
is passed through to the database. This requires two key
|
|
pieces: the predicate, and the final consumer.
|
|
|
|
The predicate is a Typed Scheme function that determines if a
|
|
string is acceptable as input to the database:
|
|
|
|
\begin{schemedisplay}
|
|
(: sql-safe? (String -> Boolean))
|
|
(define (sql-safe? s) ELIDED)
|
|
\end{schemedisplay}
|
|
|
|
No special type system machinery is required to write and use such a
|
|
predicate. One more step is needed, however, to turn this predicate
|
|
into a refinement type:
|
|
|
|
\begin{schemedisplay}
|
|
(declare-refinement sql-safe?)
|
|
\end{schemedisplay}
|
|
|
|
\noindent
|
|
This declaration puts the function \scheme|sql-safe?|
|
|
into the refinement environment $\Sigma$ in the formalization of refinement types,
|
|
with the addition that it changes the type of \scheme|sql-safe?| to be
|
|
a predicate for \scheme|(Refinement sql-safe? String)|.
|
|
|
|
With this refinement type, we can specify the desired type of our
|
|
query function:
|
|
|
|
\begin{schemedisplay}
|
|
(: query ((Refinement sql-safe? String) -> (Listof Result)))
|
|
(define (query user-name)
|
|
(run-query
|
|
(string-append
|
|
"SELECT * FROM users WHERE name = '" user-name "';")))
|
|
\end{schemedisplay}
|
|
\noindent
|
|
Since \scheme|(Refinement sql-safe? String)| is a subtype of
|
|
\scheme|String|, \scheme|user-name| can be used directly as an
|
|
argument to \scheme|string-append|.
|
|
|
|
We can also write a \scheme|sanitize| function that performs the
|
|
necessary escaping, and use the \scheme|sql-safe?| function and
|
|
refinement types for static and dynamic verification:
|
|
|
|
\begin{schemedisplay}
|
|
(: sanitize (String -> (Refinement sql-safe? String)))
|
|
(define (sanitize s)
|
|
(define s* (string-map escape-char s))
|
|
(if (sql-safe? s*)
|
|
s*
|
|
(error "escape failed")))
|
|
\end{schemedisplay}
|
|
\noindent
|
|
The only function that is added to the trusted computing
|
|
base is the definition of \scheme|sql-safe?|, which can be provided by
|
|
the database vendor. Everything else is up to the programmer.
|
|
|
|
\paragraph{Alternative Solutions}
|
|
|
|
Another solution to this problem, common in other languages, would have \scheme|sanitize| be
|
|
defined in a different module, with \scheme|SQLSafeString| as an
|
|
opaque exported type. Unfortunately, this requires using an accessor
|
|
whenever a \scheme|SQLSafeString| is used in a context that expects a
|
|
string (such as \scheme|string-append|). The use of our style of refinement types
|
|
avoids both the dynamic cost of wrapping in a new type, as well as the
|
|
programmer burden of managing these wrappers and their corresponding
|
|
accessors.
|
|
|
|
\end{schemeregion}
|