TE
科技回声
首页24小时热榜最新最佳问答展示工作
GitHubTwitter
首页

科技回声

基于 Next.js 构建的科技新闻平台,提供全球科技新闻和讨论内容。

GitHubTwitter

首页

首页最新最佳问答展示工作

资源链接

HackerNews API原版 HackerNewsNext.js

© 2025 科技回声. 版权所有。

Catching integer overflows with template metaprogramming (2015)

88 点作者 jgeralnik大约 8 年前

7 条评论

DannyBee大约 8 年前
&quot;Some day, I would like to design a language that gets this right. But for the moment, I remain focused on Sandstorm.io. Hopefully someone will beat me to it. Hint hint. &quot;<p>Some language already did beat him to it: Ada<p><a href="http:&#x2F;&#x2F;www.ada-auth.org&#x2F;standards&#x2F;12rat&#x2F;html&#x2F;Rat12-2-4.html" rel="nofollow">http:&#x2F;&#x2F;www.ada-auth.org&#x2F;standards&#x2F;12rat&#x2F;html&#x2F;Rat12-2-4.html</a><p>Ada&#x27;s rules for type invariants check them in all the places you would expect, and are straightforward to use.<p>It&#x27;s about as correct as you can get without it being impossible to compute :)
评论 #13964627 未加载
评论 #13964566 未加载
评论 #13964527 未加载
评论 #13964535 未加载
michaelt大约 8 年前
<p><pre><code> Why don’t programming languages do this? </code></pre> I worked on a contribution to clang-analyser a few months ago - one of the things I learned was (1) No-one likes code analysers that raise false alarms and (2) it&#x27;s really difficult not to raise false alarms. For example, consider checking this program for divide-by-zero bugs:<p><pre><code> for (int i=-99999 ; i&lt;99999 ; i+=2) { printf(&quot;%d\n&quot;, 100&#x2F;i); } for (int i=-100000 ; i&lt;100000 ; i+=2) { printf(&quot;%d\n&quot;, 100&#x2F;i); } </code></pre> A programmer can clearly see that in the first loop there is no divide-by-zero as i will jump directly from -1 to +1 - whereas in the second loop the counter will hit 0 and trigger a divide-by-zero.<p>But for a static analyser, your options are:<p>1. Model i as a single value, and simulate all ~400,000 passes through the loops. Slow - you basically have to run the program at compile time.<p>2. Same but truncate the simulation after, say, 20 loops on the assumption that most bugs would have been found on the first few passes. This misses the bug in the second loop.<p>3. Model i as &quot;Integer in the range -99,999 to +99,999&quot; and generate a false alarm on the first loop.<p>4. Support arbitrarily complex symbolic values. Difficult - as the value of a variable might depend on complicated business logic.<p>I guess the benefit of starting a new programming language is you can choose option 3 and say &quot;Working code is illegal, deal with it&quot; from the start.
评论 #13968097 未加载
staticassertion大约 8 年前
That&#x27;s a pretty impressive response - committing to fuzzing with AFL, improving current fuzzing test coverage, adding new coding guidelines, and a paid security audit.<p>In regards to 4 (valgrind) perhaps utilizing other sanitizers would be a good idea.<p>Awesome that they tested whether those methods would actually have caught this bug - and multiple did. That&#x27;s a smart metric.<p>And a writeup about TMP and compile time safety to boot.<p>I&#x27;m struggling to come up with anything more that I&#x27;d want in a disclosure.
评论 #13964425 未加载
jbapple大约 8 年前
Two other ways of checking integer bound invariants:<p>1. Undefined behavior sanitizer, which checks integer overflows at run-time, like INT_MAX + 1. Can optionally check other invariants; see <a href="https:&#x2F;&#x2F;gcc.gnu.org&#x2F;onlinedocs&#x2F;gcc&#x2F;Instrumentation-Options.html" rel="nofollow">https:&#x2F;&#x2F;gcc.gnu.org&#x2F;onlinedocs&#x2F;gcc&#x2F;Instrumentation-Options.h...</a> and <a href="https:&#x2F;&#x2F;clang.llvm.org&#x2F;docs&#x2F;UndefinedBehaviorSanitizer.html" rel="nofollow">https:&#x2F;&#x2F;clang.llvm.org&#x2F;docs&#x2F;UndefinedBehaviorSanitizer.html</a>.<p>2. Abstract interpretation - using a lot of constraint solver cycles and enough math to choke a dinosaur, you can check some integer bounds at compile time &quot;relationally&quot;, like knowing that x &lt; y. See, for example, &quot;Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses&quot;: <a href="https:&#x2F;&#x2F;www.microsoft.com&#x2F;en-us&#x2F;research&#x2F;publication&#x2F;pentagons-a-weakly-relational-abstract-domain-for-the-efficient-validation-of-array-accesses&#x2F;" rel="nofollow">https:&#x2F;&#x2F;www.microsoft.com&#x2F;en-us&#x2F;research&#x2F;publication&#x2F;pentago...</a>. I&#x27;m not sure, but that code might be available in <a href="https:&#x2F;&#x2F;github.com&#x2F;Microsoft&#x2F;CodeContracts" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;Microsoft&#x2F;CodeContracts</a>.
评论 #13964608 未加载
norswap大约 8 年前
&gt; Some day, I would like to design a language that gets this right. But for the moment, I remain focused on Sandstorm.io. Hopefully someone will beat me to it.<p>Two language that do it: Whiley (<a href="http:&#x2F;&#x2F;whiley.org&#x2F;" rel="nofollow">http:&#x2F;&#x2F;whiley.org&#x2F;</a>) and Dafny (<a href="http:&#x2F;&#x2F;rise4fun.com&#x2F;dafny" rel="nofollow">http:&#x2F;&#x2F;rise4fun.com&#x2F;dafny</a>).<p>I expect (but not sure) that the proving power is about the same as what can be achieved by template meta-programming.
winstonewert大约 8 年前
I&#x27;m unclear on how this would work out practically. Cases where my integers belong to a fixed range seems rare. I&#x27;d like to have seen more discussion of how it caught the bugs it did.
评论 #13965370 未加载
danschumann大约 8 年前
Boo I thought it was a reference to fictional Tom Parris&#x27;s holodeck program