Introduction

As a proof of concept for verifiable forensic certificates, we have developed a verifiable formalization of forensic reports. The forensic reports are for a computer intrusion investigation challenge organized by the Honeynet Project.

Honeynet Project's Challenge

The Honeynet Project's Scan of the Month #15 is:

The Challenge:
On 15 March. 2001, a Linux honeypot was successfully compromised, a rootkit was download to the / partition and then deleted from the system. Your mission is to find and recover the deleted rootkit. If you are not sure where to begin on conducting this forensic analysis and recover the rootkit, we highly reccommend you start with the Forensic Challenge. The steps you will have to follow for the rootkit recovery are similar to the steps discussed there. We have posted only the / partion for download to keep this challenge simple. The compressed image is 13MB, (honeynet.tar.gz) MD5=0dff8fb9fe022ea80d8f1a4e4ae33e21. Once you have downloaded, untarred, and unzipped the partition image, it will be 255 MB and the checksum should be MD5=5a8ebf5725b15e563c825be85f2f852e.
  1. Show step by step how you identify and recover the deleted rootkit from the / partition.
  2. What files make up the deleted rootkit?

Two of the top five reports submitted as challenge entries were:

Coq Formalization and Verification of Forensic Reports

The rootkit presence from Borland's report and the timeline from Lee's report have a Coq formalization in this code (git repository). The Coq doc documentation can be used to browse results and definitions.

In this Coq code, the primary results are:

The relevant part of the Ext2 image file (from honeynet.tar.gz) used in these results is:

The formalization and verification, including performance, is discussed in the MS thesis listed below.

Bibliography
Last modified: February 10, 2014