Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
---
layout: post
author: Pascal Cuoq
date: 2011-06-02 17:52 +0200
categories: skein value
format: xhtml
title: "Skein tutorial, part 7: not dead, but resting"
summary:
---
{% raw %}
<p>Do you remember the Skein tutorial? It went off to a good start (it started this blog) and then was never really completed. I blame <strong>laziness</strong>. Looking back at that first post, I notice that indeed, before Boron, we were shipping software without documentation (just think! Ahem). At the time, I also thought that the extended tutorial would be over in a couple of posts, a mistake I have learnt not to make any more. September 2010, those were the days…</p>
<h2>The story so far</h2>
<p>The solution provided in <a href="/index.php?post/2010/11/21/Value-analysis-tutorial%2C-part-4">this post</a> was one of two promised solutions. It was in fact my own solution. While conceiving it I was determined not to look at Skein's source code. I could claim that this was to make the verification method completely independent of the code which is obviously good. It allows for instance to swap in another implementation — say another entry in the NIST SHA3 contest — and hopefully to verify it just by relaunching the same script. The true reason I didn't want to look at the code is more likely written in bold at the top of this post.</p>
<p>Because I didn't want to look at Skein's source code my solution involved the meta-argument that you can cover all possible executions of the loop</p>
<pre> while (Frama_C_interval(0 1))
{
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
}
</pre>
<p>by analyzing instead the two pieces of code below which between them do all the same things:</p>
<pre> while (Frama_C_interval(0 1))
{
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
}
</pre>
<pre> arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
while (Frama_C_interval(0 1))
{
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
}
</pre>
<h2>The alternate solution</h2>
<p>In July 2010 I was teaching at <a href="http://flolac.iis.sinica.edu.tw/flolac10/en/start.html">the FLOLAC summer school</a> and I was lucky to have <a href="http://joshkos.blogspot.com/">Josh Ko</a> as my Teaching Assistant. He did not have my prejudices against looking at the code being verified. The alternate and better solution that follows is his.</p>
<p>We determined when we elaborated the solution based on pairing the calls to <code>Skein_256_Update()</code> that the issue was the field <code>skein_context.h.bCnt</code>
that contained <code>0</code> before the first iteration and alternately <code>16</code> or <code>32</code> after that.
Pairing the calls to <code>Skein_256_Update()</code> was one way to force similar calls to be analyzed together and prevent a loss of precision caused by not knowing whether <code>skein_context.h.bCnt</code> was <code>16</code> or <code>32</code>. Josh Ko's solution instead prevents the loss of precision by nudging the value analysis into studying these cases separately by way of an annotation inside <code>Skein_256_Update()</code>:</p>
<pre>--- skein.c.orig 2011-06-02 21:06:29.000000000 +0200
+++ skein.c 2011-06-02 21:06:50.000000000 +0200
@@ -159 6 +159 8 @@
Skein_Assert(ctx->h.bCnt <= SKEIN_256_BLOCK_BYTES SKEIN_FAIL); /* catch uninitialized context */
+ /*@ assert ctx->h.bCnt == 0 || ctx->h.bCnt == 16 || ctx->h.bCnt == 32 ; */
+
/* process full blocks if any */
if (msgByteCnt + ctx->h.bCnt > SKEIN_256_BLOCK_BYTES)
{
</pre>
<p>We have seen how to provide useful annotations in <a href="/index.php?post/2011/03/26/Helping-the-value-analysis-2">this post</a>. The above annotation is another example. With it we can use this <code>main()</code>:</p>
<pre>void main(void)
{
int i;
u08b_t hash[HASHLEN];
Skein_256_Ctxt_t skein_context;
Skein_256_Init(&skein_context HASHLEN * 8);
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
while (Frama_C_interval(0 1))
{
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
}
Skein_256_Final( &skein_context hash);
}
</pre>
<pre>$ time frama-c -val -slevel 1000 -slevel-function main:0 *.c -cpp-command "gcc -m32 -C -E -I. " > log2
real 1m48.218s
user 1m45.133s
sys 0m1.325s
</pre>
<p>This single <code>main()</code> cover all the programs with n>=2 calls to <code>Skein_256_Update(… 80)</code>:</p>
<pre>$ grep ssert log2
skein.c:162:[value] Assertion got status valid.
</pre>
<p>And that's that: no alarm is emitted and the annotation that we provided for the value analysis is verified before being used (so it is not an assumption).</p>
<p>For the sake of completeness the cases of 0 and 1 calls to <code>Skein_256_Update(… 80)</code> should also be checked separately. We have done that before so there is no need to repeat it here.</p>
<h2>Generalizing</h2>
<p>The advantage of the method presented in this post over the previous one is that it can more easily be generalized to different buffer lengths passed to <code>Skein_256_Update()</code>. The more complete verification that I <a href="/index.php?post/2010/11/22/Value-analysis-tutorial%2C-part-5%3A-jumping-to-conclusions">last alluded to</a> uses among other annotations the assertion below.</p>
<pre> /*@ assert
ctx->h.bCnt == 0 || ctx->h.bCnt == 1 ||
ctx->h.bCnt == 2 || ctx->h.bCnt == 3 ||
ctx->h.bCnt == 4 || ctx->h.bCnt == 5 ||
ctx->h.bCnt == 6 || ctx->h.bCnt == 7 ||
ctx->h.bCnt == 8 || ctx->h.bCnt == 9 ||
ctx->h.bCnt == 10 || ctx->h.bCnt == 11 ||
ctx->h.bCnt == 12 || ctx->h.bCnt == 13 ||
ctx->h.bCnt == 14 || ctx->h.bCnt == 15 ||
ctx->h.bCnt == 16 || ctx->h.bCnt == 17 ||
ctx->h.bCnt == 18 || ctx->h.bCnt == 19 ||
ctx->h.bCnt == 20 || ctx->h.bCnt == 21 ||
ctx->h.bCnt == 22 || ctx->h.bCnt == 23 ||
ctx->h.bCnt == 24 || ctx->h.bCnt == 25 ||
ctx->h.bCnt == 26 || ctx->h.bCnt == 27 ||
ctx->h.bCnt == 28 || ctx->h.bCnt == 29 ||
ctx->h.bCnt == 30 || ctx->h.bCnt == 31 ||
ctx->h.bCnt == 32 ; */
</pre>" <p>Do you remember the Skein tutorial? It went off to a good start (it started this blog) and then was never really completed. I blame <strong>laziness</strong>. Looking back at that first post, I notice that indeed, before Boron, we were shipping software without documentation (just think! Ahem). At the time, I also thought that the extended tutorial would be over in a couple of posts, a mistake I have learnt not to make any more. September 2010, those were the days…</p>
<h2>The story so far</h2>
<p>The solution provided in <a href="/index.php?post/2010/11/21/Value-analysis-tutorial%2C-part-4">this post</a> was one of two promised solutions. It was in fact my own solution. While conceiving it I was determined not to look at Skein's source code. I could claim that this was to make the verification method completely independent of the code which is obviously good. It allows for instance to swap in another implementation — say another entry in the NIST SHA3 contest — and hopefully to verify it just by relaunching the same script. The true reason I didn't want to look at the code is more likely written in bold at the top of this post.</p>
<p>Because I didn't want to look at Skein's source code my solution involved the meta-argument that you can cover all possible executions of the loop</p>
<pre> while (Frama_C_interval(0 1))
{
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
}
</pre>
<p>by analyzing instead the two pieces of code below which between them do all the same things:</p>
<pre> while (Frama_C_interval(0 1))
{
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
}
</pre>
<pre> arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
while (Frama_C_interval(0 1))
{
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
}
</pre>
<h2>The alternate solution</h2>
<p>In July 2010 I was teaching at <a href="http://flolac.iis.sinica.edu.tw/flolac10/en/start.html">the FLOLAC summer school</a> and I was lucky to have <a href="http://joshkos.blogspot.com/">Josh Ko</a> as my Teaching Assistant. He did not have my prejudices against looking at the code being verified. The alternate and better solution that follows is his.</p>
<p>We determined when we elaborated the solution based on pairing the calls to <code>Skein_256_Update()</code> that the issue was the field <code>skein_context.h.bCnt</code>
that contained <code>0</code> before the first iteration and alternately <code>16</code> or <code>32</code> after that.
Pairing the calls to <code>Skein_256_Update()</code> was one way to force similar calls to be analyzed together and prevent a loss of precision caused by not knowing whether <code>skein_context.h.bCnt</code> was <code>16</code> or <code>32</code>. Josh Ko's solution instead prevents the loss of precision by nudging the value analysis into studying these cases separately by way of an annotation inside <code>Skein_256_Update()</code>:</p>
<pre>--- skein.c.orig 2011-06-02 21:06:29.000000000 +0200
+++ skein.c 2011-06-02 21:06:50.000000000 +0200
@@ -159 6 +159 8 @@
Skein_Assert(ctx->h.bCnt <= SKEIN_256_BLOCK_BYTES SKEIN_FAIL); /* catch uninitialized context */
+ /*@ assert ctx->h.bCnt == 0 || ctx->h.bCnt == 16 || ctx->h.bCnt == 32 ; */
+
/* process full blocks if any */
if (msgByteCnt + ctx->h.bCnt > SKEIN_256_BLOCK_BYTES)
{
</pre>
<p>We have seen how to provide useful annotations in <a href="/index.php?post/2011/03/26/Helping-the-value-analysis-2">this post</a>. The above annotation is another example. With it we can use this <code>main()</code>:</p>
<pre>void main(void)
{
int i;
u08b_t hash[HASHLEN];
Skein_256_Ctxt_t skein_context;
Skein_256_Init(&skein_context HASHLEN * 8);
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
while (Frama_C_interval(0 1))
{
arbitrarize_msg();
Skein_256_Update(&skein_context msg 80);
}
Skein_256_Final( &skein_context hash);
}
</pre>
<pre>$ time frama-c -val -slevel 1000 -slevel-function main:0 *.c -cpp-command "gcc -m32 -C -E -I. " > log2
real 1m48.218s
user 1m45.133s
sys 0m1.325s
</pre>
<p>This single <code>main()</code> cover all the programs with n>=2 calls to <code>Skein_256_Update(… 80)</code>:</p>
<pre>$ grep ssert log2
skein.c:162:[value] Assertion got status valid.
</pre>
<p>And that's that: no alarm is emitted and the annotation that we provided for the value analysis is verified before being used (so it is not an assumption).</p>
<p>For the sake of completeness the cases of 0 and 1 calls to <code>Skein_256_Update(… 80)</code> should also be checked separately. We have done that before so there is no need to repeat it here.</p>
<h2>Generalizing</h2>
<p>The advantage of the method presented in this post over the previous one is that it can more easily be generalized to different buffer lengths passed to <code>Skein_256_Update()</code>. The more complete verification that I <a href="/index.php?post/2010/11/22/Value-analysis-tutorial%2C-part-5%3A-jumping-to-conclusions">last alluded to</a> uses among other annotations the assertion below.</p>
<pre> /*@ assert
ctx->h.bCnt == 0 || ctx->h.bCnt == 1 ||
ctx->h.bCnt == 2 || ctx->h.bCnt == 3 ||
ctx->h.bCnt == 4 || ctx->h.bCnt == 5 ||
ctx->h.bCnt == 6 || ctx->h.bCnt == 7 ||
ctx->h.bCnt == 8 || ctx->h.bCnt == 9 ||
ctx->h.bCnt == 10 || ctx->h.bCnt == 11 ||
ctx->h.bCnt == 12 || ctx->h.bCnt == 13 ||
ctx->h.bCnt == 14 || ctx->h.bCnt == 15 ||
ctx->h.bCnt == 16 || ctx->h.bCnt == 17 ||
ctx->h.bCnt == 18 || ctx->h.bCnt == 19 ||
ctx->h.bCnt == 20 || ctx->h.bCnt == 21 ||
ctx->h.bCnt == 22 || ctx->h.bCnt == 23 ||
ctx->h.bCnt == 24 || ctx->h.bCnt == 25 ||
ctx->h.bCnt == 26 || ctx->h.bCnt == 27 ||
ctx->h.bCnt == 28 || ctx->h.bCnt == 29 ||
ctx->h.bCnt == 30 || ctx->h.bCnt == 31 ||
ctx->h.bCnt == 32 ; */
</pre>"
{% endraw %}