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.017s):
let u : user = {is_admin = false; username = "diego"; email = "shannon"}
Refuted
proof attempt
ground_instances:1
definitions:0
inductions:0
search_time:
0.017s
details:
Expand
smt_stats:
num checks:3
arith-make-feasible:3
arith-max-columns:4
rlimit count:1576
mk clause:10
datatype occurs check:30
seq add axiom:9
mk bool var:104
bv bit2core:72
decisions:4
seq num reductions:8
propagations:4
interface eqs:3
conflicts:1
datatype accessor ax:6
datatype constructor ax:1
seq extensionality:3
num allocs:735071
final checks:5
added eqs:36
memory:5.370000
max memory:5.370000
Expand
  • start[0.017s]
      let (_x_0 : bool) = ( :var_0: ).is_admin in
      _x_0 = 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 _x_0 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:
    let (_x_0 : bool) = ( :var_0: ).is_admin in
    _x_0
    || (if _x_0 || List.exists ((fun u au -> au = u.username) ( :var_0: )) …
        then Authed else Not_authed)
       = Not_authed
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • unroll
        expr:
        (|`List.exists { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: string -> bool) (anon_fun.ge…
        expansions:
        • Sat (Some let u : user = {is_admin = false; username = "diego"; email = "shannon"} )

        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]:
        Modular_decomp.top ~prune:true "get_auth_result" [@@program];;
        
        Out[6]:
        - : Top_result.modular_decomposition =
        (decomp (get_auth_result path, u
         :regions (<reg 0>, <reg 1>, <reg 2>, <reg 3>, <reg 4>, <reg 5>, <reg 6>))
        
        Regions details

        No group selected.

        • Concrete regions are numbered
        • Unnumbered regions are groups whose children share a particular constraint
        • Click on a region to view its details
        • Double click on a region to zoom in on it
        • Shift+double click to zoom out
        • Hit escape to reset back to the top
        decomp of (get_auth_result path, u
        Reg_idConstraintsInvariant
        6
        • String.prefix (String.append "/user/" u.username) path
        • String.prefix "/user/" path
        Authed
        5
        • not (String.prefix (String.append "/user/" u.username) path)
        • String.prefix "/user/" path
        Not_authed
        4
        • u.is_admin
        • String.prefix "/admin" path
        • not (String.prefix "/user/" path)
        Authed
        3
        • "shannon" = u.username
        • not ("diego" = u.username)
        • not u.is_admin
        • String.prefix "/admin" path
        • not (String.prefix "/user/" path)
        Authed
        2
        • "diego" = u.username
        • not u.is_admin
        • String.prefix "/admin" path
        • not (String.prefix "/user/" path)
        Authed
        1
        • not ("shannon" = u.username)
        • not ("diego" = u.username)
        • not u.is_admin
        • String.prefix "/admin" path
        • not (String.prefix "/user/" path)
        Not_authed
        0
        • not (String.prefix "/admin" path)
        • not (String.prefix "/user/" path)
        Authed