Control FormalVerification

A device that can store, process, transmit or receive data.

Represents a process (usually implemented by software running on a Host) that can read, update or create data, or exchange data with other processes.

The software for device Host has been analysed by independent experts using formal methods and shown to be free of bugs. It is therefore guaranteed to work correctly for arbitrary (even malicious) inputs. However, this is only possible for simple devices. Note that it does not prevent bugs that are present being discovered and exploited by attackers, so it is a prior mitigation only which is ignored in current (run-time) risk calculations (although in principle no vulnerabilities should ever be found).

The software for process Process has been analysed by independent experts using formal methods and shown to be free of bugs. It is therefore guaranteed to work correctly for arbitrary (even malicious) inputs. However, this is only possible for simple processes. Note that it does not prevent bugs that are present being discovered and exploited by attackers, so it is a prior mitigation only which is ignored in current (run-time) risk calculations (although in principle no vulnerabilities should ever be found).