GitHub - cmc333333/forensics-thesis-code: Accompanying Code for Depaul Thesis

This is a formalization of a honeynet challenge (http://old.honeynet.org/scans/scan15/).

It includes two proofs (in honeynet.v):

lee_honeynet_file - Recreate a timeline proposed by Lee in his Honeynet submission, then prove that the hard drive provided satisfies that timeline
borland_honeynet_file - Recreate evidence Borland provided in his Honeynet submission (i.e. that a malicious, deleted gzip was found on the file system)

To execute, run the make file, then step through honeynet.v with Coq.

For more details see formalized-forensics.pdf, a paper written to accompany this code.

Name		Name	Last commit message	Last commit date
Latest commit History 49 Commits
tools		tools
.gitignore		.gitignore
Byte.v		Byte.v
ByteData.v		ByteData.v
DiskSubset.v		DiskSubset.v
Ext2.v		Ext2.v
Fetch.v		Fetch.v
File.v		File.v
FileData.v		FileData.v
FileIds.v		FileIds.v
FileNames.v		FileNames.v
FileTypes.v		FileTypes.v
HoneynetDefinitions.v		HoneynetDefinitions.v
Makefile		Makefile
README.md		README.md
StringOps.v		StringOps.v
Tar.v		Tar.v
Timeline.v		Timeline.v
Util.v		Util.v
example_images.v		example_images.v
formalized-forensics.pdf		formalized-forensics.pdf
honeynet.v		honeynet.v
reflection_example.v		reflection_example.v
tar_runtimes.v		tar_runtimes.v
timing.py		timing.py

cmc333333/forensics-thesis-code