Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Defining the Undefinedness of C (2015) [pdf]

fsl.cs.illinois.edu

Post reply on HN
Print view View original

71–80 of 91 posts

Re: Defining the Undefinedness of C (2015) [pdf]

#71

Post by nickpsecurity »

tom_mellior wrote: post #65
nickpsecurity wrote: post #22

That team’s awesome. One of few groups in formal methods using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. They also build their own modified logic called matching logic on top that they claim is better than separation logic. http://www.kframework.org/index.php/Main_Page More interesting, their use of these tools allowed them to make their C s…

> using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. This statement is close to nonsensical. What are you comparing it to? Where is a comparable executable semantics project in Coq or Isabelle? This is great work, and they are definitely using the right tool for the job. But the field of "formal methods" is enormous, and you seem to be saying t…

"What are you comparing it to? Where is a comparable executable semantics project in Coq or Isabelle?"

In the others, they tend to do formal semantics of interpreters or compilers then extract them to ML or something. This group uses an executable, rewriting engine to do an executable semantics of a lot of languages which seems to require less people. Perhaps they're doing less on the verification side but what I've seen make me think more should try such methods.

Most work I see posted in formal methods isn't done with rewriting tools like Maude. The ones I see use it get some interesting results for effort put in such as the SCOOP verification. So, I took the time to highlight that they use a different approach with quite a bit of tooling to use that people might want to look into trying. My 2nd reply, jcranmer, had exactly the kind of positive experience I was thinking readers might get out of a follow-up.

"But the field of "formal methods" is enormous, and you seem to be saying that apples are better than oranges."

You wouldn't notice it's enormous with the number of people that use a relatively-small set of tools. Convergence is usually good since ecosystems get built that can make new work easier. Coq and Isabelle/HOL are good examples where people keep plugging in prior work to new work. There's also quite a few more that don't get as much attention. Hence, me highlighting two (Maude and K) that had a series of practical results out of research using it.

Re: Defining the Undefinedness of C (2015) [pdf]

#72

Post by solidangle »

tom_mellior wrote: post #65
nickpsecurity wrote: post #22

That team’s awesome. One of few groups in formal methods using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. They also build their own modified logic called matching logic on top that they claim is better than separation logic. http://www.kframework.org/index.php/Main_Page More interesting, their use of these tools allowed them to make their C s…

> using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. This statement is close to nonsensical. What are you comparing it to? Where is a comparable executable semantics project in Coq or Isabelle? This is great work, and they are definitely using the right tool for the job. But the field of "formal methods" is enormous, and you seem to be saying t…

Here is a Coq formalization of C11: http://robbertkrebbers.nl/research/ch2o/ It only covers a large fragment of C11, but they formalized the operational, axiomatic, and executable semantics and proved that these correspond to each other.

Re: Defining the Undefinedness of C (2015) [pdf]

#73

Post by nickpsecurity »

jcranmer wrote: post #50
nickpsecurity wrote: post #22

That team’s awesome. One of few groups in formal methods using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. They also build their own modified logic called matching logic on top that they claim is better than separation logic. http://www.kframework.org/index.php/Main_Page More interesting, their use of these tools allowed them to make their C s…

One of the courses I took involved working with K, and I certainly left the course thinking "I would love to use this tool in the future if I had a project to do with it." It is actually a fairly amazing tool, even if the instructions for using it involve "start by downloading it again, because we keep fixing bugs". One problem with building semantics for Rust is that the language doesn't have a sufficiently formal s…

"It is actually a fairly amazing tool"

Since I watch formal methods from a distance, I can't really tell how good their approach is versus Microsoft's VCC w/ separation logic, Coq specifications, and so on. I just note they seem to have it easier than most like Coq with their method more flexible than separation logic. How hard do you think it would be for a non-formalist programmer to learn K and start modeling interpreters or compilers in it? Anything you'd recommend to a person trying to learn it in terms of background material?

"One problem with building semantics for Rust is that the language doesn't have a sufficiently formal specification yet."

My solution there was to make the semantics represent the current state of Rust and/or LLVM at any moment. They got the advantage of being the standard implementation. So, the spec needs to do what they do so users don't get inconsistent behavior. Then, the spec work might find errors or validate proposals that can feed back into reference implementations. Finally, as with KCC, the implementation might be useful for looking into compiler errors or subversions.

Re: Defining the Undefinedness of C (2015) [pdf]

#74

Post by pjmlp »

pcwalton wrote: post #54
duneroadrunner wrote: post #46

Earlier quoted context omitted.

I can't say for certain why none of the "safer C"s have caught on, but I can say that they all have significant compromises and/or impracticalities. Often, performance cost is one of them. Today though, you can use the safe numerics[1] library along with SaferCPlusPlus[2] (shameless plug) as a high performance solution to address undefined behavior in your C code. This solution preserves most of your C code intact, a…

There have been lots of solutions like "SaferCPlusPlus" over the years. In my view, the real reasons why these have not been adopted widely are (1) aversion to any sort of runtime overhead greater than zero; (2) cognitive overhead of introducing new language machinery, type-level or otherwise; (3) interoperability with existing code; (4) few people want to be the first to adopt these kinds of tools in production due…

Interesting chart, in spite of what I answered to you in another thread, I have noticed something along those lines regarding C++'s usage on UWP.

From the prominent place it used to have at Microsoft presentations, back in the Windows 8 days, it seems to be relegated to high performance UWP componentes and all presentations, including HoloLens ones, are done in C#.

Also the pivoting from Google regarding Brillo, by dropping the planned C++ Framework and instead adopting the Java one from Android.

Re: Defining the Undefinedness of C (2015) [pdf]

#75

Post by tom_mellior »

solidangle wrote: post #72
tom_mellior wrote: post #65

Earlier quoted context omitted.

> using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. This statement is close to nonsensical. What are you comparing it to? Where is a comparable executable semantics project in Coq or Isabelle? This is great work, and they are definitely using the right tool for the job. But the field of "formal methods" is enormous, and you seem to be saying t…

Here is a Coq formalization of C11: http://robbertkrebbers.nl/research/ch2o/ It only covers a large fragment of C11, but they formalized the operational, axiomatic, and executable semantics and proved that these correspond to each other.

Yes, and there are other formalizations as well. But none of them (as far as I am aware) formalize the undefined parts in the way the featured article does. I think comparing projects with different goals and then saying "the differences must be due to the tools used" isn't solid reasoning.

Re: Defining the Undefinedness of C (2015) [pdf]

#76

Post by jcranmer »

nickpsecurity wrote: post #73
jcranmer wrote: post #50

Earlier quoted context omitted.

One of the courses I took involved working with K, and I certainly left the course thinking "I would love to use this tool in the future if I had a project to do with it." It is actually a fairly amazing tool, even if the instructions for using it involve "start by downloading it again, because we keep fixing bugs". One problem with building semantics for Rust is that the language doesn't have a sufficiently formal s…

"It is actually a fairly amazing tool" Since I watch formal methods from a distance, I can't really tell how good their approach is versus Microsoft's VCC w/ separation logic, Coq specifications, and so on. I just note they seem to have it easier than most like Coq with their method more flexible than separation logic. How hard do you think it would be for a non-formalist programmer to learn K and start modeling inte…

> How hard do you think it would be for a non-formalist programmer to learn K and start modeling interpreters or compilers in it? Anything you'd recommend to a person trying to learn it in terms of background material?

I am not a formal methods person, and I have very little grounding in it. I still felt quite happy using it and came out of the course thinking "gee, I think I might actually like to use this if I ever had a need," which is the opposite anecdote I hear from people using a lot of formal methods tooling. You probably do need a basic grounding in semantics, though, things like big-step versus small-step operational semantics. Beyond that, the K framework itself has a tutorial on actually building the semantics in K. (See http://www.kframework.org/index.php/K_Tutorial and the corresponding directories within its tooling).

Re: Defining the Undefinedness of C (2015) [pdf]

#77

Post by marcosdumay »

fundabulousrIII wrote: post #26

My good god. Do you actually believe that this scenario reflects a weakness in C or a C compiler?

Integral overflow and volatile memory are the 2 most problematic kinds of UB in C, because they can appear basically everywhere. Rust has features to deal with them.

Re: Defining the Undefinedness of C (2015) [pdf]

#78

Post by nayuki »

iainmerrick wrote: post #37
littlestymaar wrote: post #25

Earlier quoted context omitted.

Undefined means : the compiler can omit this case and assume it never happens. Take integer overflow for instance: an implementation-defined behavior means in case of overflow the compiler can either wrap, crash, or have a saturation at max value. Undefined behavior means the compiler can assume it doesn't happen and optimize with this information in mind. For instance, the following code : for(i = 0; i With the unde…

That's a good example, thanks! Reminds me of the Java binary search bug: https://research.googleblog.com/2006/06/extra-extra-read-all... I think the correct code here would be something like: for (j = i; j Or something like that. Obviously that's rather awkward, with the risk of a sneaky off-by-one bug. (Edit to add: heh, just noticed I'm assuming max+1 won't overflow!) It would be great to have a C-like language tha…

The silver lining in that Java bug is that it is guaranteed to compute the same wrong negative indexes every time on every platform, and it is guaranteed to throw ArrayIndexOutOfBoundsException when the array is attempted to be indexed. Though the code is wrong, it is at least consistently wrong and loudly wrong. The same cannot be said for a similar bug implemented in C.

Re: Defining the Undefinedness of C (2015) [pdf]

#79

Post by duneroadrunner »

pcwalton wrote: post #54
duneroadrunner wrote: post #46

Earlier quoted context omitted.

I can't say for certain why none of the "safer C"s have caught on, but I can say that they all have significant compromises and/or impracticalities. Often, performance cost is one of them. Today though, you can use the safe numerics[1] library along with SaferCPlusPlus[2] (shameless plug) as a high performance solution to address undefined behavior in your C code. This solution preserves most of your C code intact, a…

There have been lots of solutions like "SaferCPlusPlus" over the years. In my view, the real reasons why these have not been adopted widely are (1) aversion to any sort of runtime overhead greater than zero; (2) cognitive overhead of introducing new language machinery, type-level or otherwise; (3) interoperability with existing code; (4) few people want to be the first to adopt these kinds of tools in production due…

I think all your points are probably right (and insightful). But I think in this case the (immediate) goal isn't really popular adoption of this solution by existing C (or maybe even C++) programmers.

In part, it is simply a practical, relatively low cost solution to address the problem of invalid memory access in existing C/C++ code (and thus, for example, remote code execution vulnerabilities in internet facing code). Clearly we've still not reached the point where critical internet infrastructure vulnerabilities are perceived as costly enough to justify actually solving the problem (as you say in point 5). And collectively, we've not yet concluded that cheaper mitigation techniques aren't a "good enough" solution. At least for now.

But the costs (of critical vulnerabilities) are still going up, and there may come a time when some conclude that they have no choice but to properly address the issue. And some may opt for the least expensive option (i.e. something like SaferCPlusPlus rather than a full rewrite in another memory-safe language).

Of course, more appealing solutions might emerge before that time comes.

But there is also a longer term goal. I see a safe dialect of C++ (like SaferCPlusPlus) perhaps relevant in a future where code is liberated from the "language silo" it's trapped in, via auto-translators. For example, I don't expect C programmers to switch to SaferCPlusPlus en masse (although I'll probably continue to encourage it :). The idea is that legacy C code would be auto-translated to SaferCPlusPlus (with or without the support/consent of the original author). Kind of like how the tor guys used to build their ("safer") version of firefox with the sanitizers enabled[1], and didn't need the permission of the firefox developers to do it.

But it doesn't have to be restricted to just legacy C/C++ code. Modern C++ is so powerful that lots of languages could be translated to (a safe dialect of) it. I think. Presumably C++ would be a more appealing language if it had easy access to, say, all the existing Java code via auto-translation. This of course would apply to any language, but I think its power and performance makes C++ a good target for auto-translation. I'm sure other languages would make good targets too.

Basically, in the future I expect auto-translation quality to be a bigger factor wrt language relevance than marketing or mind-share.

[1] https://blog.torproject.org/blog/tor-browser-55a4-hardened-r...

Re: Defining the Undefinedness of C (2015) [pdf]

#80

Post by Retra »

gh02t wrote: post #60
littlestymaar wrote: post #25

Earlier quoted context omitted.

Undefined means : the compiler can omit this case and assume it never happens. Take integer overflow for instance: an implementation-defined behavior means in case of overflow the compiler can either wrap, crash, or have a saturation at max value. Undefined behavior means the compiler can assume it doesn't happen and optimize with this information in mind. For instance, the following code : for(i = 0; i With the unde…

> Undefined means : the compiler can omit this case and assume it never happens. That's not the whole picture though. The standard actually says that anything can happen in undefined cases. > However, if any such execution contains an undefined operation, this International Standard places no requirement on the implementation executing that program with that input (not even with regard to operations preceding the fir…

Anything can happen because the compiler will assume it doesn't happen. "Undefined behavior" essentially means, "If you try to do this, you have written a program that is not C, and you should not be handing it to a C compiler expecting it to do anything correctly."

If you were to try to write a program that accurately detected whether the given input is a meaningful C program, you'd have to solve the Halting Problem (and more, once you take IO into account.) Thus undefined behavior must exist in the places where your program is syntactically valid but has no definite semantics. (And you can't enumerate all of these places in a Turing complete language.)

Not even a C compiler will be able to tell you if it actually has been given C code; all it can say is "I parsed it, and here're some semantics for it."

Post reply on HN