| As part of a team project modeling computer system vulnerabilities and cyberattacks, this research focused on Petri net models and validation methods for them. First, the chosen target, Metasploitable, was scanned for vulnerabilities, which were matched to Common Attack Pattern Enumeration and Classification (CAPEC) entries. For a preliminary validation, the models were compared with the entries. Then a dynamic validation was applied to two models of CAPEC entries and to one model of a known backdoor, Ingreslock. Three experimental cyberattacks were compared with their respective models, giving partial validation. The results of the comparison show that this dynamic method was only sufficient to validate a specific sequence of each attack. Formal analysis of Petri net properties proved to be more suited to verification of the model, rather than validation. |
