Formalization of computer input and output: the Hadley model

Current digital evidence acquisition tools are effective, but are tested rather than formally proven correct. We assert that the forensics community will benefit in evidentiary ways and the scientific community will benefit in practical ways by moving beyond simple testing of systems to a formal model. To this end, we present a hierarchical model of peripheral input to and output from von Neumann computers, patterned after the Open Systems Interconnection model of networking. The Hadley model categorizes all components of peripheral input and output in terms of data flow; with constructive aspects concentrated in the data flow between primary memory and the computer sides of peripherals' interfaces. The constructive domain of Hadley is eventually expandable to all areas of the I/O hierarchy, allowing for a full view of peripheral input and output and enhancing the forensics community's capabilities to analyze, obtain, and give evidentiary force to data.