Analysing Web-app Authentication Logic

When writing and refactoring we often have to make a lot of assumptions about how our code works. Here we'll look at some example authentication logic written in OCaml that you might find a standard web application codebase, and use Imandra as a tool to analyse it.

Let's imagine our system currently has a user represented by this type:

In [1]:
type user = 
{ is_admin: bool
; username: string
; email: string
}
Out[1]:
type user = { is_admin : bool; username : string; email : string; }

Right. Let's take a look at the core of the authentication logic itself.

In [2]:
type auth_result = Authed | Not_authed;;

let get_auth_result (path: string) (u : user) : auth_result =
    if String.prefix "/user/" path then
        if String.prefix ("/user/" ^ u.username) path then
            Authed
        else
            Not_authed
    else if String.prefix "/admin" path then
        if u.is_admin then
            Authed
        else
            (* Temporary hack to give co-founder accounts admin access for the demo! - DA 06/05/15 *)
            if List.exists (fun au -> au = u.username) ["diego"; "shannon"] then
                Authed
            else
                Not_authed
    else
        Authed
Out[2]:
type auth_result = Authed | Not_authed
val get_auth_result : string -> user -> auth_result = <fun>

There's even a few tests (although they are a bit rusty...)!

In [3]:
type test_result = Pass | Fail;;
let run_test f = if f then Pass else Fail;;
Out[3]:
type test_result = Pass | Fail
val run_test : bool -> test_result = <fun>
In [4]:
run_test ((get_auth_result "/" { username = "test"; email = "email"; is_admin = false }) = Authed);;
run_test ((get_auth_result "/admin" { username = "test"; email = "email"; is_admin = false }) = Not_authed);;
run_test ((get_auth_result "/admin" { username = "test"; email = "email"; is_admin = true }) = Authed);;
run_test ((get_auth_result "/user/paula" { username = "joe"; email = "email"; is_admin = false } = Not_authed));;
run_test ((get_auth_result "/user/paula" { username = "paula"; email = "email"; is_admin = false } = Authed));;
run_test ((get_auth_result "/user/paula/profile" { username = "paula"; email = "email"; is_admin = false } = Authed));;
Out[4]:
- : test_result = Pass
- : test_result = Pass
- : test_result = Pass
- : test_result = Pass
- : test_result = Pass
- : test_result = Pass

However the tests haven't quite covered all the cases. Let's use Imandra to verify a few things. Note that we've got tests for is_admin = true (test 2) and is_admin = false (test 3) on the /admin route above, but this only checks that these inputs give the desired outcome, and not that all inputs do. So let's verify that all non-admin users are not authenticated for the admin area.

In [5]:
verify (fun u -> u.is_admin = false ==> (get_auth_result "/admin" u) = Not_authed)
Out[5]:
- : user -> bool = <fun>
module CX : sig val u : user end
Counterexample (after 1 steps, 0.011s):
 let u = {is_admin = false; username = "diego"; email = "diego"}
Refuted
proof attempt
ground_instances1
definitions0
inductions0
search_time
0.011s
details
Expand
smt_stats
num checks3
rlimit count721
mk clause10
datatype occurs check24
seq add axiom2
mk bool var24
decisions4
seq num reductions10
propagations4
interface eqs2
conflicts1
datatype accessor ax6
datatype constructor ax1
seq extensionality2
num allocs1367341659
final checks4
added eqs20
del clause6
memory16.280000
max memory18.750000
Expand
  • start[0.011s]
      :var_0:.is_admin = false
      ==> (if String.prefix "/user/" "/admin"
           then
             if String.prefix (String.append "/user/" :var_0:.username) "/admin"
             then Authed else Not_authed
           else
           if String.prefix "/admin" "/admin"
           then
             if :var_0:.is_admin then Authed
             else
             if List.exists ((fun u au -> au = u.username) :var_0:) …
             then Authed else Not_authed
           else Authed)
          = Not_authed
  • simplify

    into
    :var_0:.is_admin
    || (if :var_0:.is_admin then Authed
        else
        if List.exists ((fun u au -> au = u.username) :var_0:)
           ("diego" :: (… :: …))
        then Authed else Not_authed)
       = Not_authed
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|`List.exists (anon_fun.get_auth_result.0 (u : user))[0]`_2466|
          u_2459
          (|::_3| "diego" (|::_3| …
        expansions
        • Sat (Some let u = {is_admin = false; username = "diego"; email = "diego"} )

        This verification fails, and Imandra gives us an example input that violates the assumption we gave it - we hadn't considered the users added by the 'temporary hack' code path in our tests!

        We can also ask for a decomposition of all the regions in the get_auth_result function, which gives us an idea of the various conditions and complexity:

        In [6]:
        Decompose.by_simp_ctx ~compound:false "get_auth_result";;
        
        Out[6]:
        - : Imandra_reasoning.Decompose.t list =
        [<region>; <region>; <region>; <region>; <region>; <region>; <region>]
        
        Regions details
        No group selected.
        ConstraintsInvariant
        • not (String.prefix (String.append "/user/" u.username) path)
        • String.prefix "/user/" path
        F = Not_authed
        • not (String.prefix (String.append "/user/" u.username) path)
        • not (String.prefix "/user/" path)
        • not (String.prefix "/admin" path)
        F = Authed
        • not (String.prefix (String.append "/user/" u.username) path)
        • not (String.prefix "/user/" path)
        • String.prefix "/admin" path
        • not u.is_admin
        • not ("diego" = u.username)
        • not ("shannon" = u.username)
        F = Not_authed
        • not (String.prefix (String.append "/user/" u.username) path)
        • not (String.prefix "/user/" path)
        • String.prefix "/admin" path
        • not u.is_admin
        • not ("diego" = u.username)
        • "shannon" = u.username
        F = Authed
        • not (String.prefix (String.append "/user/" u.username) path)
        • not (String.prefix "/user/" path)
        • String.prefix "/admin" path
        • not u.is_admin
        • "diego" = u.username
        F = Authed
        • not (String.prefix (String.append "/user/" u.username) path)
        • not (String.prefix "/user/" path)
        • String.prefix "/admin" path
        • u.is_admin
        F = Authed
        • String.prefix (String.append "/user/" u.username) path
        F = Authed