Model Checking
The model checking is launched through PAT 3.5.0 (https://pat.comp.nus.edu.sg/), with the default setting.
In total, we identify four vulnerabilities (V1-V4). We present the model checking results below.
The following outputs are collected from PAT console output.
V1: searching with first witness trace using depth-first search
********Verification Result********
The Assertion (system() |= [] requirement_3) is NOT valid.
A counterexample is presented as follows.
<init -> load_policy -> pre_read_from_1 -> init_part_i -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> pre_read_from_0 -> init_part_i -> [int_choice] -> load_policy -> pre_read_from_1 -> init_part_i -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> pre_read_from_0 -> init_part_i -> [int_choice] -> update_to_1>
********Environment Variables********
Variables:
participant1_policy=[1, 1, 0, 0];
participant2_policy=[1, 1, 0, 0];
node2_policy=[0, 0, 1, 1];
node1_policy_1=[1, 1, 0, 0];
gk_node1_access=[1, 1, 1, 1];
gk_node2_access=[1, 1, 1, 1];
security_file_location=1;
standard_policy=[0, 0, 1, 1];
msg_enc=1;
node_security_file_usage=[0, 0];
participant_initialization_status=[1, 1];
node_initialization_status = [1,1];
********Verification Setting********
Admissible Behavior: All
Method: Refinement Based Safety Analysis using DFS - The LTL formula is a safety property!
System Abstraction: False
********Verification Statistics********
Visited States:181
Total Transitions:1297
Time Used:0.0204223s
Estimated Memory Used:14730.304KB
V2: searching with first witness trace using depth-first search
********Verification Result********
The Assertion (system() |= [] requirement_4) is NOT valid.
A counterexample is presented as follows.
<init -> load_policy -> pre_read_from_1 -> init_part_i -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> pre_read_from_0 -> init_part_i -> [int_choice] -> load_policy -> pre_read_from_1 -> init_part_i -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> topic2_msg_chl!1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> node_part_chl2[0]!1 -> [int_choice] -> pre_read_from_0 -> init_part_i -> [int_choice] -> update_to_1>
********Environment Variables********
Variables:
participant1_policy=[1, 1, 0, 0];
participant2_policy=[1, 1, 0, 0];
node2_policy=[1, 1, 0, 0];
node1_policy_1=[0, 0, 1, 1];
gk_node1_access=[1, 1, 1, 1];
gk_node2_access=[1, 1, 1, 1];
security_file_location=1;
standard_policy=[0, 0, 1, 1];
msg_enc=1;
node_security_file_usage=[0, 1];
participant_initialization_status=[1, 1];
node_initialization_status = [1,1];
********Verification Setting********
Admissible Behavior: All
Method: Refinement Based Safety Analysis using DFS - The LTL formula is a safety property!
System Abstraction: False
********Verification Statistics********
Visited States:181
Total Transitions:1297
Time Used:0.0235982s
Estimated Memory Used:14656.28KB
V3: searching with first witness trace using depth-first search
The Assertion (system() |= [] requirement_6) is NOT valid.
A counterexample is presented as follows.
<init -> load_policy -> pre_read_from_1 -> init_part_i -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> node_part_chl2[1]!1 -> [int_choice] -> pre_read_from_0 -> init_part_i -> [int_choice] -> load_policy -> pre_read_from_1 -> init_part_i -> [int_choice] -> node_part_chl2[0]!1 -> node_part_chl2[0]?1
********Verification Setting********
Admissible Behavior: All
Method: Refinement Based Safety Analysis using DFS - The LTL formula is a safety property!
System Abstraction: False
********Environment Variables********
Variables:
participant1_policy=[1, 1, 0, 0];
participant2_policy=[1, 1, 0, 0];
node2_policy=[0, 0, 1, 1];
node1_policy_1=[1, 1, 0, 0];
gk_node1_access=[1, 1, 1, 1];
gk_node2_access=[1, 1, 1, 1];
security_file_location=1;
standard_policy=[0, 0, 1, 1];
msg_enc=0;
node_security_file_usage=[0, 0];
participant_initialization_status=[1, 1];
node_initialization_status = [1,1];
********Verification Statistics********
Visited States:102
Total Transitions:835
Time Used:0.0048383s
Estimated Memory Used:13238.616KB
V4: searching with the first witness trace using depth-first search
The Assertion (system() |= [] requirement_6) is NOT valid.
A counterexample is presented as follows.
<init -> load_policy -> pre_read_from_1 -> [int_choice] -> node_part_chl2[1]!1 -> initPart0 -> initPart1
********Verification Setting********
Admissible Behavior: All
Method: Refinement Based Safety Analysis using DFS - The LTL formula is a safety property!
System Abstraction: False
********Environment Variables********
Variables:
participant1_policy=[1, 1, 0, 0];
participant2_policy=[1, 1, 0, 0];
node2_policy=[1, 1, 0, 0];
node1_policy_1=[1, 1, 0, 0];
gk_node1_access=[1, 1, 1, 1];
gk_node2_access=[1, 1, 1, 1];
security_file_location=1;
standard_policy=[0, 0, 1, 1];
msg_enc=1;
node_security_file_usage=[0, 0];
participant_initialization_status=[1, 1];
node_initialization_status = [1,1];
********Verification Statistics********
Visited States:407
Total Transitions:616
Time Used:0.0056975s
Estimated Memory Used:13150.576KB