High-level events of forensic timelines using runtime verification

Timeline reconstruction is the aspect of digital forensics that concerns itself with assembling a timeline of events from a recovered image. The timeline usually consists of a list of very basic events, such as file creation or file changes. These lists are ordered chronologically and include the time at which each event has taken place. In the case of large systems such as a smartphone device, the lists are generally huge, and therefore very difficult to analyse manually.

Various techniques are used to build timelines of a higher level, i.e., events that would be more understandable to humans. This project consists of identifying scenarios that took place on an Android device using runtime verification. A tool called LARVA was used for the task, while any high-risk scenarios that could take place on Android were described using finite-state automata (FSA). This is essentially a formal way of describing the different scenarios that could take place. The FSA was programmed into LARVA to act as the basis for runtime verification. An example of these sequence of events is when a user downloads files from the internet (for example from Google Drive) and installs them on the device.

The identified scenarios could be used by digital forensics investigators to track down methods that malware could have employed to infiltrate the system. Using the previous example, if an application were to be downloaded from Google Drive and installed on the Android device, it could be unsafe, as opposed to applications downloaded from the Android market.