======== Examples ======== This section describes the examples included in the releases of N-PAT. Network Security ================ Description ########### Suppose there is a cluster of computation nodes, and each node can be in one of the three states: *safe*, *compromised*, and *isolated*. Initially, each node is safe, but it has a chance to be *hacked*, which changes the state of the node to compromised. When a node is compromised, it can either be *patched*, which will make the node safe again, or be *isolated*, which will disconnect the node from the cluster. If a node is isolated, then it loses the connection to other nodes and thus cannot contribute to the computational power of the cluster. When the node is isolated, it has a chance to be \emph{recovered}, which will make it safe again. Otherwise, the node stays isolated, in which case we increase down nodes counter, i.e., the number of nodes that are offline, by 1. For simplicity, we assume that the hacking of each node is independent. We model two types of nodes: \emph{normal} node and \emph{premium} node, where the latter has a higher chance to be patched when it is compromised and a higher chance to be recovered when it is isolated. Nested Model Checking ##################### We break the model description down into two levels of abstraction: the node level and the cluster level. The idea is to create more modular models so that the model for a node can be used for both normal nodes and for premium nodes, and potentially can be used in future developments of other models. At the node level, we study the common properties of the two types of nodes, and try to generalise the model so that the model-checking result is exactly what we need at the cluster level. As the cluster manager, we only need to know whether a node is offline or not. Therefore, besides safe, isolated, and compromised, we give a node two additional states: ``ok`` and ``down``. Each node is initialised to be in the safe state. When a node stays isolated, we change its state to ``down``, and when it is not hacked/patched/recovered, we change its state to ``ok``. At the cluster level, we abstract the notion of a node into only two states: ``ok`` and ``down``. The probability of going to these two states will be given by the model-checking results from the node level. If a node is down, then we increment the down nodes counter. We iterates through each node in the cluster and checks whether the node is offline. We report that the cluster is in critical condition if at least half of the nodes in the cluster are offline. The NML expression that model this study is given in ``network.nm``, it relies on the meta-PCSP# models ``cluster.mpcsp`` and ``node.mpcsp`` which respectively models the cluster and node levels. Content of ``network.nm``: :: let NumberOfNode = 16, pNormalDown = (let pHack=500,pPatch=100,pRecover=200 in let pSafe=1000-pHack,pIsolate=1000-pPatch,pDefaultIso=1000-pRecover in mmc("node.mpcsp" where pHack=pHack, pSafe=pSafe, pPatch=pPatch, pIsolate=pIsolate, pRecover=pRecover, pDefaultIso=pDefaultIso)), pPremDown = (let pHack=800,pPatch=200,pRecover=300 in let pSafe=1000-pHack,pIsolate=1000-pPatch,pDefaultIso=1000-pRecover in mmc("node.mpcsp" where pHack=pHack, pSafe=pSafe, pPatch=pPatch, pIsolate=pIsolate, pRecover=pRecover, pDefaultIso=pDefaultIso)) in let NumberOfNormalNode = ((NumberOfNode * 4) / 5), pNormalOk = 1000 - pNormalDown, pPremOk = 1000 - pPremDown in mmc("cluster.mpcsp" where NumberOfNode=NumberOfNode, NumberOfNormalNode=NumberOfNormalNode, pNormalOk=pNormalOk, pNormalDown=pNormalDown, pNormalOk=pNormalOk, pNormalDown=pNormalDown, pPremOk=pPremOk, pPremDown=pPremDown) The source code of this example is avaiable`here `_. Simple Model Checking ##################### We include a flat version of the same study case: ``flatMetwork.nm``. Notice that the high-level bindings are the same as in the NML expression of ``network.nm``. The nested and flat models both give the same results when provided with the same parameters. Thie flat version is introduced to illustrate the greater scalability of the nested models. Further, it motivates the advantages of N-PAT over traditional model checking tools that support only flat models. Content of ``flatNetwork.nm``: :: let NumberOfNode = 16, pNormalHack=500, pNormalPatch=100, pNormalRecover=200, pPremHack=800, pPremPatch=200, pPremRecover=300 in let NumberOfNormalNode = ((NumberOfNode * 4) / 5), pNormalSafe=1000-pNormalHack, pNormalIsolate=1000-pNormalPatch, pNormalDefaultIso=1000-pNormalRecover, pPremSafe=1000-pPremHack, pPremIsolate=1000-pPremPatch, pPremDefaultIso=1000-pPremRecover in mmc("flatCluster.mpcsp" where NumberOfNode=NumberOfNode, NumberOfNormalNode=NumberOfNormalNode, pNormalHack=pNormalHack, pNormalPatch=pNormalPatch, pNormalRecover=pNormalRecover, pPremHack=pPremHack, pPremPatch=pPremPatch, pPremRecover=pPremRecover, pNormalSafe=pNormalSafe, pNormalIsolate=pNormalIsolate, pNormalDefaultIso=pNormalDefaultIso, pPremSafe=pPremSafe, pPremIsolate=pPremIsolate, pPremDefaultIso=pPremDefaultIso)