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
---
layout: post
author: Pascal Cuoq
date: 2010-10-15 08:44 +0200
categories: skein value
format: xhtml
title: "Value analysis tutorial, part 3: answering one quiz"
summary:
---
{% raw %}
<p>This is another episode in the advanced value analysis tutorial. The first episode was <a href="/skein/value/2010/09/30/Progress-of-the-value-analysis-tutorial2" hreflang="en">here</a> and the second one <a href="/index.php?post/2010/10/07/Value-analysis-tutorial%2C-part-2" hreflang="en">here</a>.</p>
<p>There were a couple of questions left unanswered at the break. This post answers the first one.</p>
<blockquote><p>Quiz 1: continuing the study of the first five calls to <code>Skein_256_Update</code> what used to cause the warning below and what made it disappear?</p>
<p><code>lib.c:18:<a href="kernel" title="kernel">kernel</a> warning: out of bounds write. assert \valid(tmp);</code></p>
</blockquote>
<p>Value analysis messages in the log are output in order. To understand what the analysis was doing when an alarm was emitted it is recommended to look at the surrounding entries in the log. Using the command-line <code>frama-c -val -slevel 100 -slevel-function main:0 *.c > log</code> on the version of <code>main</code> without unrolling we get the following information about the circumstances that cause the value analysis to worry about line lib.c:18 in function <code>memset</code>:</p>
<pre>...
[value] Done for function Skein_256_Update
[value] computing for function Skein_256_Final <-main.
Called from main.c:44.
[value] computing for function memset <-Skein_256_Final <-main.
Called from skein.c:212.
lib.c:18:[kernel] warning: out of bounds write. assert \valid(tmp);
[value] Recording results for memset
[value] Done for function memset
...</pre>
<p>Using <code>frama-c-gui</code> to observe the value of the troublesome pointer inside <code>memset</code> we see for the <code>main</code> with unrolling:</p>
<p><code>tmp ∈ {{ &skein_context + [24..87] ; &cfg + [0..31] ;}}</code></p>
<p>Repeating the procedure for the <code>main</code> without unrolling we see:</p>
<p><code>tmp ∈ {{ &skein_context + [24..88] ; &cfg + [0..31] ;}}</code></p>
<p>It seems that the pointer causing the problem is at an offset of 88 bytes inside <code>skein_context</code>. To confirm this still while in <code>frama-c-gui</code> we can select any statement of the function <code>main</code> and use "Evaluate expression" in the contextual menu to evaluate the expression <code>sizeof(skein_context)</code>. The result is as follows:</p>
<pre>[...] all the values taken by the expression sizeof(skein_context) are contained in {88; }</pre>
<p>Note: not all C expressions can be evaluated this way but expressions of the form <code>sizeof(v)</code> can at a statement where the variable <code>v</code> is in scope. This is often useful to make sense of the offsets in bytes displayed by the value analysis.</p>
<p>So the problem is indeed that the value analysis thinks that the pointer may refer to offset 88 of <code>skein_context</code> when dereferenced inside <code>memset</code>. This address is out of range. According to the log snippet above this happens when <code>memset</code> is called from <code>Skein_256_Final</code>. The log points us to line 212 in file skein.c that is the first call in that function. This call is guarded by the following conditional and comment:</p>
<code><p>if (ctx->h.bCnt < SKEIN_256_BLOCK_BYTES) /* zero pad b[] if necessary */</p>
<p> memset(&ctx->b[ctx->h.bCnt] 0 SKEIN_256_BLOCK_BYTES - ctx->h.bCnt);</p>
</code><p>In that call the pointer argument is <code>& ctx->b[ctx->h.bCnt]</code> and the values recorded at the <code>if</code> for <code>ctx->h.bCnt</code> are {0; 16; 32; } whereas the values at the call are {0; 16; } (the analysis knows that in the case of 32 the call is not executed because the condition <code>ctx->h.bCnt < SKEIN_256_BLOCK_BYTES</code> is false).</p>
<p>If you still have the <code>frama-c-gui</code> with the results for the main with unrolling lying around you can check that in that case the values for <code>ctx->h.bCnt</code> are {16; 32; } at the <code>if</code> and { 16; } at the call.</p>
<p>This leads us to the following conclusion: the imprecision that leads to the false alarm at lib.c:18 is caused by analyzing the call to <code>memset</code> with imprecise arguments in function <code>Sein_256_Final</code>. By unrolling the first few calls to <code>Skein_256_Update</code> we also forced these calls to happen systematically and that made the analysis conditions for <code>Skein_256_Final</code> simpler. When completing the verification with separate analyses of the omitted cases the arguments to <code>memset</code> are precise again (and complementary) so the false alarm is omitted again.</p>
<p>In fact if we kept investigating in the same fashion we would find that the case <code>ctx->h.bCnt==0</code> corresponds to the absence of any call to <code>Skein_256_Update</code>. This case is indeed covered by the <code>while</code> loop in the <code>main</code> analysis context without unrolling. The alarm we obtained when analyzing that loop does not mean there is a problem with the sequence <code>Skein_256_Init(...); Skein_256_Final(...);</code> only that some peculiar values happen in this case and that analyzing this case together with the others leads to false alarms. When verifying software that has already been tested and that its authors take pride on it makes sense to heuristically assume that alarms are false alarms when investigating them. One should however remain honest and continue to investigate until the alarm is understood—ideally until the value analysis can confirm that there was no alarm after all.</p>
<p>Next time the answer to the other quiz.</p>
<p>This is another episode in the advanced value analysis tutorial. The first episode was <a href="/skein/value/2010/09/30/Progress-of-the-value-analysis-tutorial2" hreflang="en">here</a> and the second one <a href="/index.php?post/2010/10/07/Value-analysis-tutorial%2C-part-2" hreflang="en">here</a>.</p>
<p>There were a couple of questions left unanswered at the break. This post answers the first one.</p>
<blockquote><p>Quiz 1: continuing the study of the first five calls to <code>Skein_256_Update</code> what used to cause the warning below and what made it disappear?</p>
<p><code>lib.c:18:<a href="kernel" title="kernel">kernel</a> warning: out of bounds write. assert \valid(tmp);</code></p>
</blockquote>
<p>Value analysis messages in the log are output in order. To understand what the analysis was doing when an alarm was emitted it is recommended to look at the surrounding entries in the log. Using the command-line <code>frama-c -val -slevel 100 -slevel-function main:0 *.c > log</code> on the version of <code>main</code> without unrolling we get the following information about the circumstances that cause the value analysis to worry about line lib.c:18 in function <code>memset</code>:</p>
<pre>...
[value] Done for function Skein_256_Update
[value] computing for function Skein_256_Final <-main.
Called from main.c:44.
[value] computing for function memset <-Skein_256_Final <-main.
Called from skein.c:212.
lib.c:18:[kernel] warning: out of bounds write. assert \valid(tmp);
[value] Recording results for memset
[value] Done for function memset
...</pre>
<p>Using <code>frama-c-gui</code> to observe the value of the troublesome pointer inside <code>memset</code> we see for the <code>main</code> with unrolling:</p>
<p><code>tmp ∈ {{ &skein_context + [24..87] ; &cfg + [0..31] ;}}</code></p>
<p>Repeating the procedure for the <code>main</code> without unrolling we see:</p>
<p><code>tmp ∈ {{ &skein_context + [24..88] ; &cfg + [0..31] ;}}</code></p>
<p>It seems that the pointer causing the problem is at an offset of 88 bytes inside <code>skein_context</code>. To confirm this still while in <code>frama-c-gui</code> we can select any statement of the function <code>main</code> and use "Evaluate expression" in the contextual menu to evaluate the expression <code>sizeof(skein_context)</code>. The result is as follows:</p>
<pre>[...] all the values taken by the expression sizeof(skein_context) are contained in {88; }</pre>
<p>Note: not all C expressions can be evaluated this way but expressions of the form <code>sizeof(v)</code> can at a statement where the variable <code>v</code> is in scope. This is often useful to make sense of the offsets in bytes displayed by the value analysis.</p>
<p>So the problem is indeed that the value analysis thinks that the pointer may refer to offset 88 of <code>skein_context</code> when dereferenced inside <code>memset</code>. This address is out of range. According to the log snippet above this happens when <code>memset</code> is called from <code>Skein_256_Final</code>. The log points us to line 212 in file skein.c that is the first call in that function. This call is guarded by the following conditional and comment:</p>
<code><p>if (ctx->h.bCnt < SKEIN_256_BLOCK_BYTES) /* zero pad b[] if necessary */</p>
<p> memset(&ctx->b[ctx->h.bCnt] 0 SKEIN_256_BLOCK_BYTES - ctx->h.bCnt);</p>
</code><p>In that call the pointer argument is <code>& ctx->b[ctx->h.bCnt]</code> and the values recorded at the <code>if</code> for <code>ctx->h.bCnt</code> are {0; 16; 32; } whereas the values at the call are {0; 16; } (the analysis knows that in the case of 32 the call is not executed because the condition <code>ctx->h.bCnt < SKEIN_256_BLOCK_BYTES</code> is false).</p>
<p>If you still have the <code>frama-c-gui</code> with the results for the main with unrolling lying around you can check that in that case the values for <code>ctx->h.bCnt</code> are {16; 32; } at the <code>if</code> and { 16; } at the call.</p>
<p>This leads us to the following conclusion: the imprecision that leads to the false alarm at lib.c:18 is caused by analyzing the call to <code>memset</code> with imprecise arguments in function <code>Sein_256_Final</code>. By unrolling the first few calls to <code>Skein_256_Update</code> we also forced these calls to happen systematically and that made the analysis conditions for <code>Skein_256_Final</code> simpler. When completing the verification with separate analyses of the omitted cases the arguments to <code>memset</code> are precise again (and complementary) so the false alarm is omitted again.</p>
<p>In fact if we kept investigating in the same fashion we would find that the case <code>ctx->h.bCnt==0</code> corresponds to the absence of any call to <code>Skein_256_Update</code>. This case is indeed covered by the <code>while</code> loop in the <code>main</code> analysis context without unrolling. The alarm we obtained when analyzing that loop does not mean there is a problem with the sequence <code>Skein_256_Init(...); Skein_256_Final(...);</code> only that some peculiar values happen in this case and that analyzing this case together with the others leads to false alarms. When verifying software that has already been tested and that its authors take pride on it makes sense to heuristically assume that alarms are false alarms when investigating them. One should however remain honest and continue to investigate until the alarm is understood—ideally until the value analysis can confirm that there was no alarm after all.</p>
<p>Next time the answer to the other quiz.</p>
{% endraw %}