Skip to content
Snippets Groups Projects
Commit 9dd1f2d3 authored by Kristof's avatar Kristof
Browse files

- Last work on Windows Machine

parent dceab197
Branches
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 203 additions and 461 deletions
CMD Verifier/Sanity-1-log.txt
+ 8
− 53
View file @ 9dd1f2d3
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1466156939
State space representation uses minimal constraint systems

Verifying property 1 at line 6
-- Throughput: 2199 states/sec, Load: 41 states -- Throughput: 62850 states/sec, Load: 470 states -- Throughput: 74640 states/sec, Load: 5498 states -- Throughput: 77120 states/sec, Load: 8978 states -- Throughput: 82513 states/sec, Load: 11025 states -- Throughput: 78580 states/sec, Load: 17456 states -- Throughput: 79807 states/sec, Load: 19855 states -- Throughput: 77315 states/sec, Load: 20628 states -- Throughput: 82581 states/sec, Load: 21057 states -- Throughput: 85361 states/sec, Load: 18871 states -- Throughput: 80163 states/sec, Load: 18726 states  -- Property is satisfied.
Exit code : 0
Elapsed time : 9.64
Kernel time : 0.09 (1.0%)
User time : 9.45 (98.1%)
page fault # : 9509
Working set : 37312 KB
Paged pool : 42 KB
Exit code : 1
Elapsed time : 0.15
Kernel time : 0.05 (31.8%)
User time : 0.03 (21.2%)
page fault # : 1808
Working set : 6900 KB
Paged pool : 34 KB
Non-paged pool : 7 KB
Page file size : 60792 KB
Options for the verification:
Generating no trace
Search order is depth first
Using conservative space optimisation
Seed is 1466156960
State space representation uses minimal constraint systems

Verifying property 1 at line 6
 -- Property is satisfied.
Exit code : 0
Elapsed time : 0.12
Kernel time : 0.06 (52.6%)
User time : 0.02 (13.2%)
page fault # : 2107
Working set : 8228 KB
Paged pool : 42 KB
Non-paged pool : 7 KB
Page file size : 36656 KB
Options for the verification:
Generating no trace
Search order is depth first
Using conservative space optimisation
Seed is 1466158212
State space representation uses minimal constraint systems

Verifying property 1 at line 6
-- Throughput: 2200 states/sec, Load: 36 states  -- Property is satisfied.
Exit code : 0
Elapsed time : 0.16
Kernel time : 0.03 (19.4%)
User time : 0.06 (38.8%)
page fault # : 2106
Working set : 8224 KB
Paged pool : 42 KB
Non-paged pool : 7 KB
Page file size : 36656 KB
Page file size : 2664 KB
CMD Verifier/Sanity-1.bat deleted 100644 → 0
+ 0
− 2
View file @ dceab197
color 0a
TimeMem-1.0 verifyta -d ../Clocks-Test-6.xml Sanity-1.q >> Sanity-ALL-log.txt
\ No newline at end of file
CMD Verifier/Sanity-1.q deleted 100644 → 0
+ 0
− 6
View file @ dceab197
// This file was generated by hand (c) Kristof Teichel June 16 2016
/*
*/
E<> deadlock
\ No newline at end of file
CMD Verifier/Sanity-2-log.txt deleted 100644 → 0
+ 0
− 112
View file @ dceab197
NEW RUN (2 Unicast, 10 Broadcast Each)
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1466584079
State space representation uses difference bound matrices

Verifying property 1 at line 6
-- Property is satisfied.
Exit code : 0
Elapsed time : 403.95
Kernel time : 1.33 (0.3%)
User time : 388.72 (96.2%)
page fault # : 425312
Working set : 1603476 KB
Paged pool : 42 KB
Non-paged pool : 18 KB
Page file size : 1627564 KB
NEW RUN (2 Unicast, 12 Broadcast Each)
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1466585568
State space representation uses difference bound matrices

Verifying property 1 at line 6
-- Aborted.
-- Out of memory.
Exit code : 1
Elapsed time : 553.18
Kernel time : 2.40 (0.4%)
User time : 511.18 (92.4%)
page fault # : 514053
Working set : 1958440 KB
Paged pool : 42 KB
Non-paged pool : 20 KB
Page file size : 1970456 KB
NEW RUN (2 Unicast, 11 Broadcast Each)
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1466586186
State space representation uses difference bound matrices

Verifying property 1 at line 6
-- Property is satisfied.
Exit code : 0
Elapsed time : 476.23
Kernel time : 1.53 (0.3%)
User time : 457.69 (96.1%)
page fault # : 472655
Working set : 1792852 KB
Paged pool : 42 KB
Non-paged pool : 19 KB
Page file size : 1807668 KB
NEW RUN (2-10 / Int: 6, Del: 3)
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1466590424
State space representation uses difference bound matrices

Verifying property 1 at line 6
-- Aborted.
-- Out of memory. See
http://bugsy.dominic.auc.dk/cgi-bin/bugzilla/show_bug.cgi?id=63
for more information.
Exit code : 1
Elapsed time : 560.71
Kernel time : 2.18 (0.4%)
User time : 522.63 (93.2%)
page fault # : 515214
Working set : 1963084 KB
Paged pool : 42 KB
Non-paged pool : 20 KB
Page file size : 1975124 KB
NEW RUN (2-6 / Int: 6, Del: 3)
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1466591609
State space representation uses difference bound matrices

Verifying property 1 at line 6
-- Property is satisfied.
Exit code : 0
Elapsed time : 409.36
Kernel time : 1.19 (0.3%)
User time : 399.19 (97.5%)
page fault # : 446194
Working set : 1687012 KB
Paged pool : 42 KB
Non-paged pool : 18 KB
Page file size : 1707240 KB
CMD Verifier/Sanity-2.q deleted 100644 → 0
+ 0
− 6
View file @ dceab197
// This file was generated by hand (c) Kristof Teichel June 16 2016
/*
*/
A[] deadlock imply P_ClientBehavior.FINISH_PROCEDURE
\ No newline at end of file
CMD Verifier/Sanity-3-log.txt deleted 100644 → 0
+ 0
− 118
View file @ dceab197
NEW RUN [1-15], Diff-int_range
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1467730671
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Property is satisfied.
Exit code : 0
Elapsed time : 202.27
Kernel time : 0.70 (0.3%)
User time : 193.30 (95.6%)
page fault # : 283748
Working set : 1086452 KB
Paged pool : 42 KB
Non-paged pool : 14 KB
Page file size : 1083288 KB
NEW RUN [1-15], Diff-dynamic_range
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1467731088
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Property is satisfied.
Exit code : 0
Elapsed time : 43.34
Kernel time : 0.09 (0.2%)
User time : 43.23 (99.7%)
page fault # : 80584
Working set : 310808 KB
Paged pool : 42 KB
Non-paged pool : 10 KB
Page file size : 317020 KB
NEW RUN [1-15], Old
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1467731239
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Property is satisfied.
Exit code : 0
Elapsed time : 64.98
Kernel time : 0.39 (0.6%)
User time : 64.15 (98.7%)
page fault # : 97728
Working set : 371192 KB
Paged pool : 42 KB
Non-paged pool : 10 KB
Page file size : 377604 KB
NEW RUN [2-7], Old
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1467731388
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Property is NOT satisfied.
Exit code : 0
Elapsed time : 104.51
Kernel time : 0.22 (0.2%)
User time : 103.91 (99.4%)
page fault # : 135745
Working set : 519116 KB
Paged pool : 42 KB
Non-paged pool : 11 KB
Page file size : 523844 KB
NEW RUN [2-7], Diff-dynamic_range
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1467731544
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Property is NOT satisfied.
Exit code : 0
Elapsed time : 80.79
Kernel time : 0.30 (0.4%)
User time : 79.83 (98.8%)
page fault # : 112003
Working set : 424180 KB
Paged pool : 42 KB
Non-paged pool : 10 KB
Page file size : 428948 KB
NEW RUN [3-7], Diff-dynamic_range
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1467731752
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Aborted.
Out of memory.
\ No newline at end of file
CMD Verifier/Sanity-3.bat deleted 100644 → 0
+ 0
− 2
View file @ dceab197
color 0e
TimeMem-1.0 verifyta -b -S1 -C ../Clocks-Test-6.xml Sanity-3.q >> Sanity-3-log.txt
\ No newline at end of file
Clocks-Test-4.xml
+ 37
− 37
View file @ 9dd1f2d3
This diff is collapsed.
Clocks-Test-5.q
+ 16
− 1
View file @ 9dd1f2d3
......@@ -53,7 +53,22 @@ A[] P_ClientBehavior.BROADCAST_FINISHED imply (P_ClientClock.client_clock_counte
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and ((P_ClientClock.client_clock_counter - server_clock_counter > bc_interval_length) or (- P_ClientClock.client_clock_counter + server_clock_counter < bc_interval_length))
E<> P_ClientBehavior.BROADCAST_FINISHED and (P_ClientClock.client_clock_counter - server_clock_counter >= bc_interval_length)
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and (P_ClientClock.client_clock_counter - server_clock_counter <= - bc_interval_length)
/*
*/
A[] P_ClientBehavior.BROADCAST_FINISHED imply (P_ClientClock.client_clock_counter - server_clock_counter < bc_interval_length)
/*
*/
A[] P_ClientBehavior.BROADCAST_FINISHED imply (P_ClientClock.client_clock_counter - server_clock_counter > - bc_interval_length)
/*
......
Clocks-Test-6.q
+ 3
− 18
View file @ 9dd1f2d3
......@@ -58,27 +58,17 @@ A[] P_ClientBehavior.BROADCAST_FINISHED imply (client_clock_counter() - server_c
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter() - server_clock_counter <= -10) and (broadcast_repetitions_counter == 2)
E<> P_ClientBehavior.UNICAST_FINISHED and abs(client_clock_counter_diff) > 0
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter() - server_clock_counter <= -bc_interval_length) and (broadcast_repetitions_counter == 2)
E<> P_ClientBehavior.BROADCAST_FINISHED and abs(client_clock_counter_diff) >= bc_interval_length-2
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter() - server_clock_counter <= -bc_interval_length)
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter() - server_clock_counter <= -6)
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and broadcast_repetitions_counter == broadcast_repetitions_max
E<> P_ClientBehavior.BROADCAST_FINISHED and broadcast_repetitions_counter == broadcast_repetitions_max-1
/*
......@@ -87,10 +77,5 @@ E<> P_ClientBehavior.BROADCAST_FINISHED and broadcast_repetitions_counter == 2
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter - server_clock_counter < 6)
/*
*/
//NO_QUERY
Clocks-Test-6.xml
+ 73
− 66
View file @ 9dd1f2d3
This diff is collapsed.
Clocks-Test-7.q
+ 63
− 20
View file @ 9dd1f2d3
//This file was generated from (Commercial) UPPAAL 4.0.12 (rev. 4561), July 2010
/*
"Does any deadlock exist?"
*/
E<> deadlock
/*
"Does every instance of deadlock necessarily mean that either the client'S behavior diagram is finished or that the maximum timer has run out?"
Sanity: "Does every instance of deadlock necessarily mean that either the client'S behavior diagram is finished or that the maximum timer has run out?"
*/
A[] \
deadlock \
......@@ -16,12 +11,12 @@ or\
P_ClientBehavior.FINISH_TIMEOUT)
/*
"Does every run eventually go to a state where either the client's behavior diagram is finished or that the maximum timer has run out?"
Sanity: "Does every run eventually go to a state where either the client's behavior diagram is finished or that the maximum timer has run out?"
*/
A<> P_ClientBehavior.FINISH_PROCEDURE or P_ClientBehavior.FINISH_TIMEOUT
/*
"Is there a way to get to a state in which the client's behavior diagram is finished?"
Sanity: "Is there at least one way to get to a state in which the client's behavior diagram is finished?"
*/
E<> P_ClientBehavior.FINISH_PROCEDURE
......@@ -31,9 +26,20 @@ E<> P_ClientBehavior.FINISH_PROCEDURE
//NO_QUERY
/*
"Is there a state where the client believes to be in interval number at least d*(L\/D + 1) and the client's clock has drifted more than d * L from the server's clock?"
*/
E<> \
(broadcast_repetitions_counter + 1 == bc_disclosure_delay * bc_interval_length / bc_offset_max_accepted + bc_disclosure_delay)\
and\
(abs(client_clock_counter_diff) >= bc_disclosure_delay * bc_interval_length)
/*
"Is it true that whenever the client believes to be in an interval of number less than d*(L\/D + 1), its clock cannot have drifted d * L or more from the server's clock?"
*/
A[] P_ClientBehavior.UNICAST_FINISHED imply abs(client_clock_counter_diff) == 0
A[] \
(broadcast_repetitions_counter + 1 < bc_disclosure_delay * bc_interval_length / bc_offset_max_accepted + bc_disclosure_delay) \
imply \
(abs(client_clock_counter_diff) < bc_disclosure_delay * bc_interval_length)
/*
......@@ -41,20 +47,16 @@ A[] P_ClientBehavior.UNICAST_FINISHED imply abs(client_clock_counter_diff) == 0
//NO_QUERY
/*
"Does the client's clock never drift further away from the server's than the length of a TESLA interval times the disclosure delay?"
If this is true, then the model is safe against the attack.
This query is expected to be falsified for scenarios with 'vulnerable' sets of TESLA parameters, and expected to be verified for 'safe' sets of TESLA parameters.
*/
E<> \
(broadcast_repetitions_counter + 1 == bc_disclosure_delay * bc_interval_length / bc_offset_max_accepted + bc_disclosure_delay)\
and\
(abs(client_clock_counter_diff) >= bc_disclosure_delay * bc_interval_length)
A[] abs(client_clock_counter_diff) < (bc_disclosure_delay - 1) * bc_interval_length
/*
*/
A[] \
(broadcast_repetitions_counter + 1 < bc_disclosure_delay * bc_interval_length / bc_offset_max_accepted + bc_disclosure_delay) \
imply \
(abs(client_clock_counter_diff) < bc_disclosure_delay * bc_interval_length)
A[] client_clock_counter()/bc_interval_length >= server_clock_counter/bc_interval_length - 1
/*
......@@ -65,9 +67,45 @@ imply \
*/
E<>\
(server_clock_counter >= (bc_interval_length / bc_offset_max_accepted - 1 + bc_disclosure_delay) * bc_interval_length + bc_interval_length + network_delay_min) \
server_clock_counter >= ((bc_disclosure_delay-1) * bc_interval_length / bc_offset_max_accepted) * bc_interval_length\
and\
(abs(client_clock_counter_diff) >= bc_disclosure_delay * bc_interval_length)
(abs(client_clock_counter_diff) >= (bc_disclosure_delay-1) * bc_interval_length)
/*
*/
//NO_QUERY
/*
*/
A[] client_clock_counter()/bc_interval_length + 1 > server_interval_counter - bc_disclosure_delay
/*
*/
E<> client_clock_counter()/bc_interval_length + 1 <= server_interval_counter - bc_disclosure_delay
/*
*/
E<> \
broadcast_repetitions_counter == (bc_disclosure_delay - 1)*bc_interval_length/bc_offset_max_accepted + bc_disclosure_delay\
and\
client_clock_counter()/bc_interval_length + 1 <= server_interval_counter - 2
/*
*/
A[]\
broadcast_repetitions_counter < (bc_disclosure_delay - 1)*bc_interval_length/bc_offset_max_accepted + bc_disclosure_delay\
imply\
client_clock_counter()/bc_interval_length + 1 >= server_interval_counter - 1
/*
*/
//NO_QUERY
/*
......@@ -81,3 +119,8 @@ imply \
*/
//NO_QUERY
/*
*/
//NO_QUERY
Clocks-Test-7.xml
+ 3
− 20
View file @ 9dd1f2d3
......@@ -45,7 +45,7 @@ const int bc_repetitions_global_max = 20;
const int unicast_repetitions_max = 1;
int [0, unicast_repetitions_max] unicast_repetitions_counter = 0;
const int broadcast_repetitions_max = 12;
const int broadcast_repetitions_max = 13;
int[0, 2*broadcast_repetitions_max] broadcast_repetitions_counter = 0;
const int
......@@ -53,14 +53,14 @@ const int
network_delay_max = 1,
malicious_delay_max = 0,
malicious_delay_broad_max = 13,
malicious_delay_broad_max = 15,
server_computation_min = 1,
server_computation_max = 1,
clock_incrementation_value = 1,
bc_interval_regulator = 5,
bc_interval_regulator = 10,
bc_interval_length = bc_interval_regulator * clock_incrementation_value,
bc_offset_max_accepted = 1;
......@@ -84,11 +84,6 @@ zero(BC_OFFSET&amp; stack[2]) { for (i : int[0, 1])
stack[i] := 0;
}
// DERIVED DATA
// int [0, malicious_delay_broad_max] malicious_delay_broad_smart = 1;
// DYNAMICALLY CALCULATED CONSTANTS
// (Derived from the fixed constants above)
......@@ -128,12 +123,6 @@ typedef int [0, (2 * network_delay_max + server_computation_max + malicious_dela
MEASURED_OFFSET client_clock_correction = 0;
INTERVAL_COUNTER server_interval_counter = 1;
//INTERVAL_COUNTER client_interval_counter;
//int [0, server_clock_counter_max] t_server;
//int [0, client_clock_counter_max] t_client;
//int t_client;
int [0, server_clock_counter_max] server_clock_counter = 0;
int [ -4*bc_interval_length,
......@@ -142,9 +131,6 @@ int [ -4*bc_interval_length,
// CLIENT CLOCK READ FUNCTION
int client_clock_counter() {return server_clock_counter + client_clock_counter_diff;}
// FUNCTION
int sum_over(int x) {return x*(x+1)/2;}
// NETWORK VARIABLES (Unicast) //
NONCE network_nonce_unicast_request,
......@@ -187,12 +173,10 @@ int [0, client_clock_counter_max] client_t1 = 0,
TIMESTAMP client_t2 = 0,
client_t3 = 0;
// BROADCAST //
TIMESTAMP client_bc_tb = 0;
INTERVAL_COUNTER client_bc_interval;
MEASURED_OFFSET unicast_offset;
MEASURED_OFFSET broadcast_offset;
......@@ -200,7 +184,6 @@ MEASURED_DELAY broadcast_delay = network_delay_min * clock_incrementation_va
MEASURED_ROUNDTRIP unicast_roundtrip = 0;
clock propagation;</declaration><location id="id14" x="-192" y="-288"><name x="-344" y="-272">UNICAST_FINISHED</name><committed/></location><location id="id15" x="-1088" y="-992"><name x="-1240" y="-1024">BROADCAST_TIMELY</name><committed/></location><location id="id16" x="-672" y="-224" color="#ffa500"><name x="-784" y="-192">FINISH_TIMEOUT</name><committed/></location><location id="id17" x="-1120" y="-416"><name x="-1280" y="-440">BROAD_TIMELINESS</name><committed/></location><location id="id18" x="-672" y="-864"><name x="-656" y="-896">BROADCAST_AGAIN</name><committed/></location><location id="id19" x="512" y="-800" color="#ffa500"><name x="368" y="-832">FINISH_PROCEDURE</name><committed/></location><location id="id20" x="-704" y="-992"><name x="-688" y="-1024">BROADCAST_FINISHED</name><committed/></location><location id="id21" x="-192" y="-672"><name x="-184" y="-664">INITIALIZING_BROADCAST</name><committed/></location><location id="id22" x="-672" y="-416" color="#ff00ff"><name x="-648" y="-408">WAITING_FOR_BROADCAST_PACKET</name><label kind="invariant" x="-648" y="-392">client_clock_counter()
&lt;= ((unicast_repetitions_counter - 1)
* broadcast_repetitions_max
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment