Cil Evaluation

  • Supervisor Dr. Joseph Kiniry
  • Subject Area Software Engineering and Applied Formal Methods
  • Pre-requisites Good knowledge C
  • Co-requisites (things you must learn along the way) Good knowledge of UNIX (generally) and OpenBSD (specifically), static program checking, and OCaml
  • Subject Coverage Programming Languages, Compilers, Static Analysis
  • Project Type Evaluation and Report (some small amount of Design and Implementation)
  • Hardware Any computer running OpenBSD

Description

Cil is ...

Mandatory Goals

  1. Gain familiarity with OpenBSD.
  2. Gain familiarity with Cil and Cil plugins.

Discretionary Goals

  1. Analyse a single critical OpenBSD component with the new Cil plugin.
  2. Support framework and tool indefinitely and help kick-start community for such.
  3. Coauthor, submit, and publish a paper on this work.

Sources of Information and Preparatory Reading

  1. OpenBSD