Skip to content
B2R2 logo B2R2 Tutorial

Problem 3: loginme

Overview

Section titled “Overview”

Field: Symbolic execution, argv modeling, path exploration

loginme is a stripped binary that checks one command-line token and prints either Access granted or Access denied. The exercise is to model the argv input symbolically and search for a path to the success block.

Files

Section titled “Files”

Use the loginme/ directory from tutorial.zip.

It has this layout:

loginme/
  Makefile
  src/
    loginme.c
  bin/
    loginme
  strip/
    loginme

The stripped challenge binary is at strip/loginme. The unstripped rebuild is at bin/loginme. The source file and unstripped binary are provided for verification; use the stripped binary for the exercise.

Goal

Section titled “Goal”

Recover the password accepted by loginme.

Problem Description

Section titled “Problem Description”

loginme expects exactly one argv token. On success it prints:

Access granted

and exits with status 0. On failure it prints:

Access denied

and exits with status 1.

The binary first calls imported strlen and then checks byte-level constraints. Solve it with symbolic execution rather than manual string reading or branch patching.

Suggested Workflow

Section titled “Suggested Workflow”
  1. Inspect the binary’s functions and PLT entries with B2R2.
  2. Find the main-like function.
  3. In the main-like function, locate the code that checks argc and loads argv[1].
  4. From there, find the internal function call that receives the argv[1] buffer as an argument. Use that callee’s entry address as startAddr.
  5. Inspect the function at startAddr. Find the imported strlen call through strlen@plt and record that PLT address as strlenPltAddr.
  6. In the same function, identify which return path means the input was accepted. Use the basic block or instruction address on that path as endAddr.
  7. Write the symbolic execution script: create the symbolic state, model the callee’s first argument as a symbolic input buffer, register the strlen hook, and search from startAddr to endAddr.
  8. Extract a concrete token from the solver model and verify it by running the binary normally.

Starter Code

Section titled “Starter Code”

Save this as loginme.fsx in the extracted loginme/ directory:

The script below uses the Windows/NuGet Z3 reference. On Linux or macOS, replace the Microsoft.Z3 reference with the matching local Z3 reference from the Z3 setup note above.

#r "nuget: B2R2.MiddleEnd.SymbEval"
#r "nuget: B2R2.FrontEnd.Intel"
// Windows:
#r "nuget: Microsoft.Z3, 4.12.2"
// Linux x64 (Ubuntu 24.04):
// #I "z3-4.16.0-x64-glibc-2.39/bin/"
// #r "Microsoft.Z3.dll"
// Linux x64 (Ubuntu 22.04):
// #I "z3-4.12.2-x64-glibc-2.35/bin/"
// #r "Microsoft.Z3.dll"
// macOS ARM64:
// #I "z3-4.16.0-arm64-osx-15.7.3/bin/"
// #r "Microsoft.Z3.dll"
// macOS Intel:
// #I "z3-4.16.0-x64-osx-15.7.3/bin/"
// #r "Microsoft.Z3.dll"


open System.Collections.Generic
open System.IO
open Microsoft.Z3
open B2R2
open B2R2.FrontEnd
open B2R2.MiddleEnd.SymbEval


let binaryPath =
  Path.Combine(__SOURCE_DIRECTORY__, "strip", "loginme")


let startAddr =
let strlenPltAddr =
let endAddr =


let hdl = BinHandle binaryPath
let executor = SymbExecutor hdl


let state =
let accessor =


// TODO: initialize the stack and frame pointer.


// TODO: model the chosen function's first argument as a symbolic string.
// The buffer returned here is later used as the value to solve and print.
let buf =


let callHooks =
  SymbCallHookRegistry().Register(strlenPltAddr, SymbCallHooks.strlen)


let z3 =
  { new ISolver with
      member _.CheckSat smt2 =
        try
          let cfg = Dictionary<string, string>()
          cfg.Add("model", "true")
          use ctx = new Context(cfg)
          use solver = ctx.MkSolver()
          solver.FromString smt2
          solver.Check() |> string |> Ok
        with ex ->
          SolverFailure(SolverCommunicationFailure ex.Message) |> Error


      member _.GetModels smt2 =
        try
          let cfg = Dictionary<string, string>()
          cfg.Add("model", "true")
          use ctx = new Context(cfg)
          use solver = ctx.MkSolver()
          solver.FromString smt2
          if solver.Check() = Status.SATISFIABLE then
            solver.Model.ToString() |> Ok
          else Ok ""
        with ex ->
          SolverFailure(SolverCommunicationFailure ex.Message) |> Error }


let query =


let result =
  executor.Run(startAddr, state, UseCallHooks callHooks, query, CustomSolver z3)
let answer = result.GetSatisfiabilityAnswer()
let password =
printfn "Recovered password: %s" password
Section titled “Recommended References”

Run

Section titled “Run”

Run the script from the extracted loginme/ directory:

Terminal window
dotnet fsi loginme.fsx

On Unix-like systems, if the extracted binary is not executable, run:

Terminal window
chmod +x strip/loginme

If you are using Linux or macOS, make sure the Z3 #I path in loginme.fsx matches the directory you unpacked before running the script.

Solution

Section titled “Solution”
Show solution

This solution uses the Windows/NuGet Z3 reference. On Linux or macOS, replace the Microsoft.Z3 reference with the matching local Z3 reference from the Z3 setup note above.

#r "nuget: B2R2.MiddleEnd.SymbEval"
#r "nuget: B2R2.FrontEnd.Intel"
// Windows:
#r "nuget: Microsoft.Z3, 4.12.2"
// Linux x64 (Ubuntu 24.04):
// #I "z3-4.16.0-x64-glibc-2.39/bin/"
// #r "Microsoft.Z3.dll"
// Linux x64 (Ubuntu 22.04):
// #I "z3-4.12.2-x64-glibc-2.35/bin/"
// #r "Microsoft.Z3.dll"
// macOS ARM64:
// #I "z3-4.16.0-arm64-osx-15.7.3/bin/"
// #r "Microsoft.Z3.dll"
// macOS Intel:
// #I "z3-4.16.0-x64-osx-15.7.3/bin/"
// #r "Microsoft.Z3.dll"


open System.Collections.Generic
open System.IO
open Microsoft.Z3
open B2R2
open B2R2.FrontEnd
open B2R2.MiddleEnd.SymbEval


let binaryPath =
  Path.Combine(__SOURCE_DIRECTORY__, "strip", "loginme")


let startAddr = 0x401136UL
let strlenPltAddr = 0x401040UL
let endAddr = 0x401300UL


let hdl = BinHandle binaryPath
let executor = SymbExecutor hdl


let state = executor.CreateState()
let accessor = SymbStateAccessor(hdl, state)


accessor.InitializeDefaultStack()
accessor.InitializeFramePointer()


let buf = accessor.AllocateSymbolicString "password"
accessor.SetArgument(0, accessor.WordValue buf.Address)


let callHooks =
  SymbCallHookRegistry().Register(strlenPltAddr, SymbCallHooks.strlen)


let z3 =
  { new ISolver with
      member _.CheckSat smt2 =
        try
          let cfg = Dictionary<string, string>()
          cfg.Add("model", "true")
          use ctx = new Context(cfg)
          use solver = ctx.MkSolver()
          solver.FromString smt2
          solver.Check() |> string |> Ok
        with ex ->
          SolverFailure(SolverCommunicationFailure ex.Message) |> Error


      member _.GetModels smt2 =
        try
          let cfg = Dictionary<string, string>()
          cfg.Add("model", "true")
          use ctx = new Context(cfg)
          use solver = ctx.MkSolver()
          solver.FromString smt2
          if solver.Check() = Status.SATISFIABLE then
            solver.Model.ToString() |> Ok
          else Ok ""
        with ex ->
          SolverFailure(SolverCommunicationFailure ex.Message) |> Error }


let query =
  { Query = SatisfyAddress endAddr
    QueryValues = buf }


let result =
  executor.Run(startAddr, state, UseCallHooks callHooks, query, CustomSolver z3)
let answer = result.GetSatisfiabilityAnswer()
let password = answer.Model.ReadCString buf
printfn "Recovered password: %s" password

Script output:

Recovered password: icst-b2r2-tutorial

Binary run:

Terminal window
./strip/loginme icst-b2r2-tutorial
Access granted