Home

Introduction

Binah is a tool for statically verifying information flow policies across Yesod and a SQL database using Liquid Haskell's decidable refinement types. It accomplishes this by augmenting the syntax allowed in Yesod's models file to specify both refinements and policies.

Refined Example

Consider the following models file:

Blob
  xVal Int
  yVal Int

Let's add some invariants to our database model! Suppose we want the xVal to be positive and yVal to be at least as large as the xVal. We can express that using familiar Liquid Haskell syntax:

Blob
  xVal {v:Int | v >= 0}
  yVal {v:Int | v >= blobYVal}

Using the refined database library, we can guarantee that any data we select will satisfy these invariants, and it will only allow us to update our database with values that satisfy these invariants. To accomplish this, Binah will generate two files from your refined-models file:

1. A Yesod-Compliant models file
2. A list of Liquid Haskell assumptions to use during verification.
3. A program that models the SQL evaluation of the queries in Haskell (expanded upon in Select Verification).

The restricted DB library

Binah provides a minimal DB library to interact with these refined models. What it currently lacks in performance it makes up for in correctness. Binah's DB library has four functions, which supports all of the CRUD operations:

• select
• update
• delete
• insert

Select Verification

In order to express that the data queried in a select query is refined by the filters in our refinement logic, we use the -p flag in Binah to generate a program that would simulate how the query is evaluated by SQL. These programs are then reflected into the refinement logic, meaning that the generated code itself becomes its own refinements. Continuing the Blob example above, here's what the generated code might look like:

{-@ reflect evalQBlobXVal @-}
evalQBlobXVal :: PersistFilter -> Int -> Int -> Bool
evalQBlobXVal EQUAL filter given = filter == given
evalQBlobXVal LE filter given = given <= filter
evalQBlobXVal GE filter given = given <= filter

{-@ reflect evalQBlobYVal @-}
evalQBlobYVal :: PersistFilter -> Int -> Int -> Bool
evalQBlobYVal EQUAL filter given = filter == given
evalQBlobYVal LE filter given = given <= filter
evalQBlobYVal GE filter given = given <= filter

{-@ reflect evalQBlob @-}
evalQBlob :: Filter Blob typ -> Blob -> Bool
evalQBlob filter blob = case filterField filter of
    BlobXVal -> evalQBlobXVal (filterFilter filter) (filterValue filter) (xVal blob)
    BlobYVal -> evalQBlobYVal (filterFilter filter) (filterValue filter) (yVal blob)

Now, when using the select function with a filter f, the data returned when querying the Blob table would have the liquid type b:Blob | evalQBlob f b. In English, a Blob such that the evaluation of the filter would have returned true.

For that, we can propagate information from the filters into the refinement logic to be used throughout the program's verification.

Update verification

Yesod uses certain query combinators to create filters for select queries and updates for update queries. Since the only way to update a record is to use an update query, which can only be created using an update combinator, we've added refinements to each of these combinators to ensure that any update query that is created will always respect the invariants described in the DB.

The World

Sometimes, we would like to create invariants that refer to the refinements on other tables in the database. For this, we give you access to the world, a Liquid Haskell representation of the refinements on the database.

Augmented Example: Policies

More than just expressing invariants on the values of the database, Binah can be used to propagate policies about the data throughout your code. This means that if your code typechecks, the policies are always adhered to whenever accessing the data. This implies that your code has no security leaks!

Blob {\u -> isAdministrator u}
  xVal {v:Int | v >= 0} {\u -> isPresident u}
  yVal {v:Int | v >= blobYVal}

In this example, we are saying the baseline policy for accessing the Blob table is that one must be an administrator. This means that, since the yVal is lacking an additional policy, it is by default guarded by the table's policy. We then added a stricter policy to the xVal-- to access it, one must be a president AND pass the policy for the table.

These policies get propagated in the Handler monad transformer, which Binah augments in the refinement logic to also be parameterized by a policy. Thus, a Handler<p> is a Handler parameterized with some policy p, which is a function from User -> Bool. Binah ensures that the policy p is propagated everywhere the sensitive value is used, guaranteeing that it is always protected by that policy.