===========================================================================================================
README for FATHoM (FormAlizing THreat Models), a tool to define and check the consistency of threat models.
===========================================================================================================
FATHoM version 0.1. Authors: Daniele Sgandurra and Erisa Karafili (d.sgandurra@imperial.ac.uk, e.karafili@imperial.ac.uk).

-The language is defined in the file "language.p". The other ".p" files are formalization of use cases.

-We used XSB version 3.6 (Gazpatcho) of April 22, 2015, available at: http://xsb.sourceforge.net/

-To open/draw the template and threat models (XML files) we used draw.io, available at: https://www.draw.io/.

-The XML of graphic representation is converted in FATHoM language using a custom script.

-The folder "use-case-literature" includes past papers (PDF) that we have analyzed with FATHoM.

===========================================================================================================
To use FATHoM
===========================================================================================================
-Launch XSB.

-Select the paths to the files:

assert(library_directory('PATH_TO_P_FILES')).

-To use a particular threat model:

[threatModelHUKO].

-To check for inconsistency:

(inco(_X), write('X='), writeln(_X), fail; true).

-To check for compromised components:

(isUncontrolled(_X), write('X='), writeln(_X), fail; true).

-To check for protected components:

(isProtected(_X), write('X='), writeln(_X), fail; true).

===========================================================================================================
FULL EXAMPLE:
===========================================================================================================
XSB Version 3.6. (Gazpatcho) of April 22, 2015

| ?- [threatModelHUKO].
[threatModelHUKO loaded]

yes
| ?- (inco(_X), write('X='), writeln(_X), fail; true).
X=app
X=os
X=covm
X=avm
X=hypervisor

yes
------------------------------------------------
Here, we have used the inco(A), query which returns those components whose assumed states is different than the derived one.

To protect components, and to check again for consistency:
------------------------------------------------
protects(tboot, hypervisor).

yes
| ?- (inco2(_X), write('X='), writeln(_X), fail; true).
X=app
X=os
------------------------------------------------

We now need to change the assumptions on the threat model to make it consistent:

------------------------------------------------
assumedUntrusted(app).
assumedUntrusted(os). 

| ?-
(inco(_X), write('X='), writeln(_X), fail; true).

yes
------------------------------------------------
We have now an initial consistent threat model.

If we now query on the previous (stable) model for the derived compromised components, we obtain:

------------------------------------------------
| ?- derivedCompromised(A).
A = covm.
A = app.
A = os.
A = remoteAtt.
A = tenant.
------------------------------------------------

On this stable threat model, we then introduce a patch in the VMM to protect the OS.  Then, by recompiling the threat model with the new protection component, and its relation(s), we query the FATHoM tool again to check the derived Protected components. We can now see that both VMM and OS are derived as Protected:

------------------------------------------------
assumedTrusted(patchVmm).
protects(hypervisor, patchVmm, os).

| ?- derivedCompromised(A).
A = covm.
A = app.
A = remoteAtt.
A = tenant.
------------------------------------------------