Skip to content

Commit 9249b17

Browse files
JellixJellix
authored
* Changed state variable(s) to enumeration type
The two Booleans Setup_Key_Called and Nonce_Setup_Called have been replaced by an enumeration type indicating the current Phase.
1 parent 15c0630 commit 9249b17

File tree

3 files changed

+39
-33
lines changed

3 files changed

+39
-33
lines changed

‎artifacts/gnatprove.out‎

Lines changed: 15 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
date : 2017-10-23 14:52:55
1+
date : 2018-02-05 12:57:40
22
gnatprove version : 2017 (20170515)
33
host : Windows 32 bits
44
command line : gnatprove.exe --assumptions --output-header -P security.gpr
@@ -8,19 +8,19 @@ gnatprove switches : --mode=all --prover=cvc4,z3,altergo --proof=progressive --s
88
Summary of SPARK analysis
99
=========================
1010

11-
-------------------------------------------------------------------------------------------------------------------------------------
12-
SPARK Analysis results Total Flow Interval CodePeer Provers Justified Unproved
13-
-------------------------------------------------------------------------------------------------------------------------------------
14-
Data Dependencies . . . . . . .
15-
Flow Dependencies . . . . . . .
16-
Initialization 171 164 . . . 7 .
17-
Non-Aliasing . . . . . . .
18-
Run-time Checks 187 . . . 187 (CVC4 99%, Z3 1%, altergo 0%) . .
19-
Assertions 22 . . . 22 (CVC4 98%, Z3 2%) . .
20-
Functional Contracts 21 . . . 21 (CVC4 99%, Z3 1%) . .
21-
LSP Verification . . . . . . .
22-
-------------------------------------------------------------------------------------------------------------------------------------
23-
Total 401 164 (41%) . . 230 (57%) 7 (2%) .
11+
-------------------------------------------------------------------------------------------------------------------------
12+
SPARK Analysis results Total Flow Interval CodePeer Provers Justified Unproved
13+
-------------------------------------------------------------------------------------------------------------------------
14+
Data Dependencies . . . . . . .
15+
Flow Dependencies . . . . . . .
16+
Initialization 166 159 . . . 7 .
17+
Non-Aliasing . . . . . . .
18+
Run-time Checks 187 . . . 187 (CVC4 100%, Z3 0%) . .
19+
Assertions 22 . . . 22 (CVC4) . .
20+
Functional Contracts 21 . . . 21 (CVC4) . .
21+
LSP Verification . . . . . . .
22+
-------------------------------------------------------------------------------------------------------------------------
23+
Total 396 159 (40%) . . 230 (58%) 7 (2%) .
2424

2525

2626
Analyzed 2 units
@@ -52,17 +52,14 @@ effects on parameters and Global variables of Crypto.To_Unsigned depends on
5252
absence of run-time errors of Crypto.To_Unsigned depends on
5353
effects on parameters and Global variables of Interfaces.Shift_Left
5454
absence of run-time errors of Interfaces.Shift_Left
55-
in unit crypto-phelix, 26 subprograms and packages out of 26 analyzed
55+
in unit crypto-phelix, 25 subprograms and packages out of 25 analyzed
5656
Crypto.Phelix at crypto-phelix.ads:57 flow analyzed (0 errors and 0 warnings) and proved (1 checks)
5757
absence of run-time errors of Crypto.Phelix fully established
5858
Crypto.Phelix.Context at crypto-phelix.ads:72 flow analyzed (0 errors and 0 warnings) and proved (0 checks)
5959
absence of run-time errors of Crypto.Phelix.Context fully established
6060
Crypto.Phelix.Ctx_AAD_Len at crypto-phelix.ads:75 flow analyzed (0 errors and 0 warnings) and proved (0 checks)
6161
effects on parameters and Global variables of Crypto.Phelix.Ctx_AAD_Len fully established
6262
absence of run-time errors of Crypto.Phelix.Ctx_AAD_Len fully established
63-
Crypto.Phelix.Ctx_AAD_Xor at crypto-phelix.ads:371 flow analyzed (0 errors and 0 warnings) and proved (0 checks)
64-
effects on parameters and Global variables of Crypto.Phelix.Ctx_AAD_Xor fully established
65-
absence of run-time errors of Crypto.Phelix.Ctx_AAD_Xor fully established
6663
Crypto.Phelix.Ctx_I at crypto-phelix.ads:79 flow analyzed (0 errors and 0 warnings) and proved (0 checks)
6764
effects on parameters and Global variables of Crypto.Phelix.Ctx_I fully established
6865
absence of run-time errors of Crypto.Phelix.Ctx_I fully established

‎src/phelix/crypto-phelix.adb‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -182,7 +182,7 @@ package body Crypto.Phelix is
182182
Increases => Src_Idx,
183183
Increases => Dst_Idx,
184184
Increases => Dst_Nxt);
185-
pragma Loop_Invariant (Src_Idx = Source'Last - Msg_Len + 1 and
185+
pragma Loop_Invariant (Src_Idx = Source'Last - Msg_Len + 1 and
186186
Dst_Idx >= Destination'First and Dst_Idx = Destination'Last - Msg_Len + 1 and
187187
Dst_Nxt >= Destination'First and Dst_Nxt - 1 <= Destination'Last and
188188
(for all X of Destination (Destination'First .. Dst_Nxt - 1) => X in Byte));
@@ -395,7 +395,7 @@ package body Crypto.Phelix is
395395

396396
-- We finalized the stream, so the previous Nonce should never be reused.
397397
-- Ensure at least part of this condition by marking the current Nonce as invalid.
398-
This.Nonce_Set := False;
398+
This.Setup_Phase := Key_Has_Been_Setup;
399399
end Finalize;
400400

401401
--
@@ -564,8 +564,7 @@ package body Crypto.Phelix is
564564
end;
565565

566566
-- Key has been set up. Require a Nonce later.
567-
This.Key_Set := True;
568-
This.Nonce_Set := False;
567+
This.Setup_Phase := Key_Has_Been_Setup;
569568
end Setup_Key;
570569

571570
--
@@ -611,7 +610,7 @@ package body Crypto.Phelix is
611610
This.CS.I := 8;
612611

613612
-- Nonce has been set.
614-
This.Nonce_Set := True;
613+
This.Setup_Phase := Nonce_Has_Been_Setup;
615614
end Setup_Nonce;
616615

617616
end Crypto.Phelix;

‎src/phelix/crypto-phelix.ads‎

Lines changed: 20 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ is
9292
Ghost => True,
9393
Global => null;
9494

95-
-- As the order in which calls are made are important, we define some proof
95+
-- As the order in which calls are made is important, we define some proof
9696
-- functions to be used as precondition.
9797
function Setup_Key_Called (Ctx : Context) return Boolean with
9898
Ghost => True,
@@ -353,24 +353,34 @@ private
353353
AAD_Xor : Word_32; -- aadXor constant
354354
end record;
355355

356+
type Phase is (Uninitialized, Key_Has_Been_Setup, Nonce_Has_Been_Setup);
357+
-- Ensure proper call sequence. State changes are:
358+
--
359+
-- (Uninitialized)
360+
-- |
361+
-- v
362+
-- (Key_Has_Been_Setup) <-.
363+
-- | |
364+
-- v |
365+
-- (Nonce_Has_Been_Setup) |
366+
-- | |
367+
-- `--------------'
368+
356369
type Context is
357370
record
358371
KS : Key_Schedule;
359372
CS : Cipher_State;
360-
-- This state variables are merely here to ensure proper call sequences as precondition.
361-
-- Also, they need to be automatically initialized.
362-
Key_Set : Boolean := False;
363-
Nonce_Set : Boolean := False;
373+
-- This state variable is merely here to ensure proper call sequences
374+
-- as precondition.
375+
-- Also, we need it to be automatically initialized.
376+
Setup_Phase : Phase := Uninitialized;
364377
end record;
365378

366379
-- Proof functions
367380

368381
function Ctx_AAD_Len (Ctx : Context) return Stream_Count is
369382
(Ctx.CS.AAD_Len);
370383

371-
function Ctx_AAD_Xor (Ctx : Context) return Word_32 is
372-
(Ctx.CS.AAD_Xor);
373-
374384
function Ctx_I (Ctx : Context) return Word_32 is
375385
(Ctx.CS.I);
376386

@@ -384,9 +394,9 @@ private
384394
(Ctx.CS.Msg_Len);
385395

386396
function Setup_Key_Called (Ctx : Context) return Boolean is
387-
(Ctx.Key_Set);
397+
(Ctx.Setup_Phase in Key_Has_Been_Setup .. Nonce_Has_Been_Setup);
388398

389399
function Setup_Nonce_Called (Ctx : Context) return Boolean is
390-
(Ctx.Key_Set and then Ctx.Nonce_Set);
400+
(Ctx.Setup_Phase in Nonce_Has_Been_Setup);
391401

392402
end Crypto.Phelix;

0 commit comments

Comments
 (0)