Work on this exercise locally

This web app is a reference guide — you can read instructions, browse starter code, and view tests here. To actually complete the exercise, you need to work in your local development environment.

1Clone the repo: git clone https://github.com/weihaoqu/program-analysis-bootcamp-student
2Edit the starter file in your editor (VS Code, Vim, etc.) — replace failwith "TODO" with your implementation.
3Run the tests: dune runtest modules/module5-security-analysis/exercises/taint-propagation

Taint Propagation

5. Exercise 3: Taint Propagation (22 tests)

Goal: Build a forward taint propagation engine that evaluates expressions and transfers statements using an abstract taint environment.

Time: ~30 minutes

File to edit: exercises/taint-propagation/starter/taint_propagator.ml

Also provided (read-only):

  • exercises/taint-propagation/starter/taint_domain.ml -- fully implemented taint lattice (same as Exercise 1's solution)
  • exercises/taint-propagation/starter/sample_programs.ml -- test programs

Dependencies: abstract_domains, shared_ast

Architecture

taint_domain.ml (provided)     taint_propagator.ml (YOUR CODE)
+--------------------------+   +---------------------------------+
| type taint = Bot | ...   |   | module Env = MakeEnv(...)       |
| join, meet, leq, ...    |   |                                 |
| is_potentially_tainted   |   | eval_expr : Env.t -> expr       |
| propagate                |   |           -> taint              |
+--------------------------+   |                                 |
                               | transfer_stmt : Env.t -> stmt   |
hardcoded source/sanitizer     |              -> Env.t           |
lists in taint_propagator.ml   |                                 |
                               | analyze_function : func_def     |
                               |                 -> Env.t        |
                               +---------------------------------+

The Env module is created for you at the top of the file using MakeEnv. The source and sanitizer lists are hardcoded:

  • Sources: "get_param", "read_cookie", "read_input"
  • Sanitizers: "escape_sql", "html_encode", "shell_escape"

What to implement (in order)

#FunctionHint
1eval_expr env ePattern match on e: IntLit/BoolLit -> Untainted; Var x -> Env.lookup x env; BinOp(_, e1, e2) -> Taint_domain.propagate both; UnaryOp(_, e1) -> eval and return; Call(name, _) -> check source/sanitizer/unknown
2transfer_stmt env sAssign(x, e) -> Env.update x (eval_expr env e) env; If(_, t, f) -> transfer both branches, Env.join; While(_, body) -> fixpoint with widening (max 100 iterations); Return/Print -> return env; Block(stmts) -> fold
3transfer_stmts env stmtsList.fold_left transfer_stmt env stmts
4analyze_function funcInitialize each param to Taint_domain.top, then transfer_stmts the body

Run tests

dune runtest modules/module5-security-analysis/exercises/taint-propagation/

Starter output (before any implementation):

EEEEEEEEEEEEEEEEEEEEEE

All 22 tests error because eval_expr throws an exception. Unlike Exercises 1 and 2, this exercise does not hit a fatal error because the test harness catches exceptions per-test. You will see Es turn to .s as you implement functions.

The while loop fixpoint

1. Start with current env
2. Transfer the loop body to get env'
3. Join: env'' = Env.join env env'    (or Env.widen env env')
4. If Env.leq env'' env (stable), stop -- return env''
5. Otherwise, repeat from step 2 with env''
6. Safety: cap at 100 iterations to prevent infinite loops

Hint for eval_expr Call: For a Call(name, args):

  • If is_source name -> Tainted
  • If is_sanitizer name -> Untainted
  • Otherwise -> Top (unknown function, conservative)