|
Gem #83: Type-Based Security 2: Validating the Input
Author: Yannick Moy, AdaCore
Abstract:
Ada Gem #83 — Ada’s strong type system makes it quite convenient to check at compilation
time that certain security properties are verified, for example that a tainted value is
not used where a trusted one is expected, or that data is properly validated
before being used in a sensitive context (think of SQL injection attacks).
In the first Gem of this series of two, we discussed how to handle tainted
data. In this Gem, we explain how to validate the input given to an SQL
command. (For an amusing comic-strip description of what SQL injection is, see:
http://xkcd.com/327/.)
Let’s get started…
Input validation consists of checking a set of properties on the input which guarantee it is well-formed. This usually involves excluding a set of ill-formed inputs (black-list) or matching the input against an exhaustive set of well-formed patterns (white-list).
Here, we consider the task of validating an input for inclusion in an SQL command. This is a well-known defense against SQL injection attacks, where an attacker passes in a specially crafted string that is interpreted as a command rather than a plain string when executing the initial SQL command.
The basic idea is to define a new type SQL_Input derived from type String. Function Validate checks that the input is properly validated and fails if not. Function Valid_String returns the raw data inside a validated string, as follows:
package Inputs is type SQL_Input is new String; function Validate (Input : String) return SQL_Input; function Valid_String (Input : SQL_Input) return String; end Inputs;The implementation of Validate simply checks that the input string does not contain a dangerous character before returning it as an SQL_Input, while Valid_String is a simple type conversion:
with Ada.Strings.Fixed; use Ada.Strings.Fixed;
with Ada.Strings.Maps; use Ada.Strings.Maps;
package body Inputs is
Dangerous_Characters : constant Character_Set := To_Set ("""*^';&><</");
function Validate (Input : String) return SQL_Input is
begin
if Index (Input, Dangerous_Characters) /= 0 then
raise Constraint_Error
with "Invalid input " & Input & " for an SQL query ";
else
return SQL_Input (Input);
end if;
end Validate;
function Valid_String (Input : SQL_Input) return String is
begin
return String (Input);
end Valid_String;
end Inputs;
Now, this does not prevent future uses of such type conversions in the program,
whether malicious or unintended. To guard against such possibilities, we must make type
SQL_Input private. To make sure we do not ourselves inadvertently convert an
input string into a valid one in the implementation of package Inputs, we use
this opportunity to make SQL_Input a discriminated record parameterized by the
validation status.
with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;
package Inputs is
type SQL_Input (<>) is private;
function Validate (Input : String) return SQL_Input;
function Valid_String (Input : SQL_Input) return String;
function Is_Valid (Input : SQL_Input) return Boolean;
private
type SQL_Input (Validated : Boolean) is
record
case Validated is
when True =>
Valid_Input : Unbounded_String;
when False =>
Raw_Input : Unbounded_String;
end case;
end record;
end Inputs;
Each time we access field Valid_Input, a discriminant check will be performed to ensure that the operand of type SQL_Input has been validated. Observe the use of Unbounded_String for the type of the input component, which is more convenient and flexible than using a constrained string.
Note in the implementation of Validate, that instead of raising an exception when the string cannot be validated, as in the first implementation, here we create corresponding validated or invalid input values based on the result of the check against dangerous characters. Also, an Is_Valid function has been added to allow clients to query validity of an SQL_Input value.
with Ada.Strings.Fixed; use Ada.Strings.Fixed;
with Ada.Strings.Maps; use Ada.Strings.Maps;
package body Inputs is
Dangerous_Characters : constant Character_Set := To_Set ("""*^';&><</");
function Validate (Input : String) return SQL_Input is
Local_Input : constant Unbounded_String := To_Unbounded_String (Input);
begin
if Index (Input, Dangerous_Characters) /= 0 then
return (Validated => False,
Raw_Input => Local_Input);
else
return (Validated => True,
Valid_Input => Local_Input);
end if;
end Validate;
function Valid_String (Input : SQL_Input) return String is
begin
return To_String (Input.Valid_Input);
end Valid_String;
function Is_Valid (Input : SQL_Input) return Boolean is
begin
return Input.Validated;
end Is_Valid;
end Inputs;
That’s it! As long as this interface is used, no errors can result in improper input being interpreted as a command, while ensuring that future maintainers of the code won’t inadvertently be able to insert inappropriate conversions.
Of course, this minimal interface does not really provide anything other than the validation of the input. Simply having an Is_Valid function to tell whether a string is valid input data would seem to give you much the same functionality. However, you can now safely extend this package with additional capabilities, such as transformations on valid SQL inputs (for example, to optimize queries before sending them to the database), or to resolve queries faster using a local cache, and so forth. By using the private encapsulation, you are guaranteed that no client package will tamper with the validity of the SQL inputs you are manipulating.
Incidentally, the similar but distinct problem of input sanitization, where possibly invalid data is transformed into something that is known valid prior to use, can be handled in the same way.
Posted
in Ada / Ada 2005 / Ada 2012, Development Log, Devt log - Gem of the Week
Have your own idea for a Gem?
If you have an idea for a Gem you would like to contribute please feel free to contact us at: gems@adacore.com
Mattias Sjösvärd said:
Greetings,
Some simple notes (and I happily receive responses on them):
I would prefer a mix of solution 1 and 2. I would say that the flaw in the first variant is lack of abstraction and the flaw of the second variant is the possibility to create invalid values (which I personally dislike).
I think the second type variant where the Sql_Type is private with unknown discriminants is superior to the first (and I think most people agree). A nice thing with unconstrained types is that you cannot declare uninitialized instances of them. However, since it is allowed to initialize an Sql_Type instance with a value that is invalid, there is no way to hinder such invalid values to be passed on to subprograms or to be put into containers etc etc. In short, we have lost some compile time error checking and pushed the error detection into run-time. A comparison; for access arguments we have the possibility to say “not null” – but in this case there is no possibility to say “is valid” adjacent to a formal argument of the Sql_Type kind.
A new variant would be if the complete type specification of Sql_Type was “type Sql_Type is new String;”. This would fulfil the visible incomplete type in simplest possible way. If the Validate method now (like in the first example), in the invalid case raises an exception and in the valid case returns a conversion of the String argument into the Sql_Type, there is no possibility that an Sql_Type instance could be initialized with an invalid value. This also renders the Is_Valid function unnecessary and the implementation of Valid_String would be trivial to say the least.
Since neither solution manages without the use of exceptions, I prefer to have the exceptions as early as possible. The impossibility to create invalid values makes it possible to build interfaces that only accepts valid instances – compile-time ensured. This, as in the “not null” cases, makes for less error prone code and less need for explicit run-time checks.
Ada has some tremendous advantages, compared to other languages, in making the code compile-time safe. I think it is important to keep this is mind when we augment the language and built-in libraries with our own abstract data types.
Yannick Moy said:
Hi Mattias,
Your mix of variants 1 and 2 indeed provides a nice solution to the problems you mentioned for each variant alone, if raising an exception is an acceptable behavior of the program. In the cases where it is not acceptable to raise exceptions, I think the second variant is appropriate. Of course, this involves more work from the programmer, and it is more error-prone to check the result of Is_Valid at appropriate places. After all, that’s why we have exceptions in the language!
You might be interested to know that the ARG is working on ’subtype predicates’ (http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0153-1.txt?rev=1.7) which you could use to define a subtype of valid SQL inputs in the second variant, as follows:
subtype Valid_SQL_Input is SQL_Input
with Predicate => SQL_Input.Validated = True;
The corresponding checks will be done either statically by the compiler when possible, or else dynamically. Nice, don’t you think?
You might also be interested in looking at the SPARK subset of Ada, whose static rules (verified by a special tool called the Examiner) prevent any read of uninitialized data, including constrained types.
Mattias Sjösvärd said:
Thanks for your comments. I’ve been a hobby user of SPARK for a couple of years, and so I’ve used preconditions quite a lot and I find them very useful. I like them much better than raising an exception to prevent abuse of a contract (which is impossible in pure SPARK code).
The ARG work does indeed look interesting!
Yannick Moy said:
Now that I know your background, I understand better your interest in static verification! :)
Note however that it is both feasible and desirable in general to call full-Ada code (not formally verified) from SPARK code (which can be formally verified, easily for run-time errors, with more work for other properties).
Then, exceptions that can be raised in Ada for a wealth of reasons are better handled by letting them propagate to a higher level where they can be treated rather than transforming them into status codes at the Ada/SPARK boundary.
See e.g. this paper where we describe errors that we have found in Tokeneer, a project in SPARK for the NSA. Some of these errors were caused by the translation of exceptions into error codes.