These types of tools go a really long way in improving the reliability and safety of C code.
Hats off to the redhat team for putting in the effort on this. Their blog posts have been really interesting. It’s definitely changing my perception of what redhat really does.
I've always had a positive impression of redhat, but I was recently blown away with their dedication to upstreaming contributions across different open source projects. I was investigating a new Linux kernel feature that redhat contributed and saw that the same developer opened pull requests that added support for the new kernel feature in three major open source projects. And one of the projects took over a year to accept the changes, but he was persistent in reaching out, making requested changes, etc. It really shows the passion at the company to share their contributions.
I, at one time, worked on a tool, commercial and external to the compiler, that did this (among other things). Probably the most intellectually challenging job I have ever had. I am happy static analysis makes inroads into mainstream!
Few takeaways from that time: inter procedural matters: if your function reallocated a pointer passed as an argument, you want to treat it as ‘free’ regarding this argument, and conversely, if your function returns a newly allocated memory, you want to mark it as such, and so on. There is also a trade off between the breadth of the analysis and the human ability to comprehend it, author mentions 110 node path in the article.
The subject of my unfinished PhD thesis and something I hope also picks up is the combination of static and dynamic analysis, used iteratively. If your static analysis flags a suspicious path but does not have the means to figure out if it is true or not, instrument it and leave it to the dynamic analysis to run through it (the idea here that total instrumentation a la valgrind is detrimental to performance so you will get some gain from selective instrumentation). Conversely, dynamic analysis may provide some hints as to where static analysis should be applied at a greater depth and provide automatic annotation of functions with regard to their behaviour and - possibly - invariants, that help with the state explosion.
ca 2000 - 2004 I had the luck to work on a massive C/C++code base building base station / telecoms infrastructure. We had several hundred engineers contributing code with all kind of different philosophies (many grey beards who did C/C++ for decades).
Running Flexelint was part of our CI chain and also part of the internal coding standard (e.g. definition of done). There was no other time in my life where I learned so much about secure coding as I did back then. Biggest challenge was agreeing about false positives and we had 1 guy in the team who maintained the official wiki document on when a lint warning needed to go on a whitelist with an agreed description of why. The initial overhead to become lint-clean got a lot of push-back but thanks to management support we got there and you could really see how things stayed at that level even after years.
It felt at times bureaucratic or like yak shaving, but in retrospect linting was what kept the code base at a quality I haven't seen ever again since. It also ensured everyone was on the same page. Taking linting seriously required a small learning curve though and lead to some discussions here or there. These discussions were really valuable since we got to really learn from another too.
When I left and went to another project it felt like a step back where we were chasing the same old bugs due to bad coding practices and it was a major step back in my career as a dev. I miss those days.
Kudos for lint-clean, and for high-quality C/C++ programming. One of my own stories of that (coincidentally, from when I worked on dev tools for aerospace/datacomm):
https://news.ycombinator.com/item?id=21158546
You don't want that option every time since its slower. But I wonder if there would be a smart way to run it occasionally, like an option to -fanalyzer every 10th time or when the size of a source file changes a lot, etc.
> As of GCC 10, that option text is now a clickable hyperlink (again, assuming a sufficiently capable terminal)
Seems like mostly only GNOME Terminal and iTerm2. Here’s some that apparently won’t work:
- Konsole
- Kitty
- LXDE Terminal
- MATE Terminal
- hyper
- Windows Terminal
- ConEmu
- PuTTY
... so it’s kind of weird to suggest this is an accepted standard. Especially since some of the discussions in feature requests suggest they will likely not implement it due to security concerns or otherwise.
Because it can break terminals that don’t. Nothing forces you to put enough context in your link to be able to recover the URL. Unsuspecting developers who only target iTerm2 will put a link in for “Click here to complete OAuth2 flow” or something and it will be broken...
In this case it isn’t the worst problem ever. but i think support for this should probably be removed from terminal emulators unless a quorum of popular terminal emulators support it.
(Addendum: do developers actually do things that only work in virtually a single terminal emulator? Yeah. A lot of Node.JS software printed status using emoji that broke horridly on everything but macOS. It mostly works elsewhere now, and it was purely a visual problem, but I would assume many didn’t even realize what their app would’ve done in most terminal emulators. The same with hyperlinks would be a disaster.)
Someone should create a database of various terminal emulators and the features they support, so that applications would be able to look up what features are available.
We shall call it the ‘terminal capabilities library’.
Yeah, it feels like we're just doing user agent vs feature detection all over again. And the xterm thing is a real concern, since I've read that lots of terminals have indeed pretended to be xterm, leading to programs having to try to detect the real terminal identity because they set TERM=xterm but don't have 100% of xterm's features...
Yep... this is exactly the problem. In fact sometimes you are recommended to go and override $TERM in order to fix a bug. Worse, is apps that do “work” but miss features. Like it is often recommended to set your term to xterm-256color to get high color in terminal apps. It’s not a huge deal, but it is simultaneously not a situation I like or think should be encouraged.
FWIW I am quite confident you can do better progressive feature detection in terminals, but until that somehow gains traction we’re going to get a lot of “hey, how come i cant click the link?” and the answer is they are using KDE or Windows.
Yup. I use alacritty, but if I SSH I frequently have to force TERM=xterm or something because nothing knows about that. But it's fine when I SSH from in tmux... because I have tmux force TERM=screen-256color to get better color support:)
I dunno, but people are getting quite mad about me suggesting this feature should be removed, so I guess it is truly mandatory that our terminal emulators do this. Shortlinks are not good enough, phishing be damned?
Probably because some URLs are really too long and would risk to fill the screen with too many characters.
This particular instance implemented by GCC10 seems the perfect example: if your terminal has no support, you get a short string like CWE-415, which is probably enough for Google; but if your terminal does support this feature, clicking on it will immediately bring you to the right page.
Escape sequences. It's similar to the "tell the emulator about the current directory" feature that is used to open new windows on the current directory.
Does the CWD feature actually use terminal escape sequences?
I always assumed the emulator accessed the working directory of the child process (as in /proc/$PID/cwd). On my terminal the CWD feature only seems to work for the topmost shell, and symlinks get resolved.
EDIT: Linked bug report mentions OCS7 (presumably an escape sequence), as one of the ways to track CWD.
There’s a fair bit of documentation here. I’d try it but I don’t have any supported terminals on any of my machines... (usually I use kitty, but I have a couple machines with KDE and Konsole.)
Another that probably won't work is xterm (which I currently use). (And if I implement my own terminal emulator, I probably won't implement it either, as I would probably mainly implementing the features of xterm and of DEC terminals.)
Oh, that's really nice. Though, as a user one should remember: The approach described here gives up at some point. So it doesn't prove the absence of a bug class (e.g. double free), but it finds some instances. Which is already a very good thing, and hugely non-trivial.
The problem with "not giving up at some point" is the computational complexity: Analyzing big code bases takes half an eternity (days), while using huge amounts of memory (>128GB). And once you enter the "least-defined state", you either throw lots of false positives (which gives the users a hard time) or you need to "give up" (and hence potentially miss bugs).
Disclaimer: I work for a company that builds static analysis tools. I don't see this as competition, though. Our tools are used in industries where "safety-critical" is really important - so the "giving up"-part of the analysis is no option for us, and solely relying only on GCC isn't an option for our customers either ;-)
I’d be interested to know which company (if you’re free to say). IIUC, this is very different from the way Coverity (the biggest commercial player I’m aware of in this space) operates.
Interestingly, different industry seems to have its own leading tool even though they all check for the same type of risks or errors. Q-AC is extremely prevalent in the Automotive Industry, Polyspace's Code Prover is also quite popular as well.
Per Rice's theorem, it's not giving up that's not a option; it's just a question of whether you have false positives or false negatives. (To be fair, for safety-critical code, insisting on only false positives (ie treating anything you give up on as a positive) is a pretty resonable choice.)
I have to wonder if Rust is putting pressure on C/++ to have more static analysis (while at the same time blazing trails in what's possible in that space, and what's possible in terms of error message helpfulness). I think it's a great idea to start baking these things into the compiler, even if it will never be 100% free of false-negatives because of the limitations of what the language can express and guarantee. Still seems like a great way to eliminate a lot of common problems, as a default across the ecosystem instead of as an extra step.
I think you mean "false-positives". Most static analysis tools are "conservative": will throw more warnings than they can prove. But assuming they're "sound" (and don't "give up" because of time/space constraints), there'd be no "false-negatives".
Vanishingly few (maybe even zero) industrial static analysis tools are sound. FPs are too common, especially for something like C++ where common code patterns can only be soundly handled by just forcing everything to Top. Good luck with your sound interprocedural pointer analysis as soon as somebody makes an indirect call.
No I meant what I said. Virtually no tool is sound (zero false negatives, lots of false positives) because in practice false positives just make people stop using tools when they are too common.
At my previous job, we used an internally developed static analysis tool. While false positives were a problem, the team responsible for the tool took bug reports and fixed these issues. There was a way to silence false positives as well as a mode to only see new (potential) problems. Once code was clean, the false positive rate was low enough to not really be a problem.
The bar of zero false negatives is not useful for me when the alternative is to rely solely human code analysis and tests.
One thing I learned from using this tool is that static analyzers need to be able to configured to know about side effects of functions that are in libraries. For example, if a library function will free memory, it is important that there's a way to tell the analyzer about this behavior to avoid false positives about leaks.
Proper design, careful coding, static analysis, code review, and various forms of testing all have roles to play in delivering reliable code.
But you can't fix all false positives with bug reports. Its fundamental if you want soundness. And for lots of properties (like I said, pointer analysis in C++) the only scalable and sound techniques basically havoc as soon as interesting things start to happen. The community even has a term (soundiness) to describe how everybody throws out certain kinds of soundness (indirect calls through function pointers, reflection in java, tons of features in javascript, etc).
Requiring the user to add piles of annotations still sucks, even if you are smart and do something like abductive inference to identify minimally required annotations. Even something as simple as the checker framework in Java has trouble getting people to write correct annotations and has a few corner cases (what is the nullness property of a field in code reachable from a constructor, for example). Nobody does this stuff correctly for something like dataflow annotations on methods.
I've got a PhD in this and develop a static analysis tool for my job. I've never seen a productionized, fully sound tool for general purpose static analysis of general programs that solves problems more difficult that slightly augmented type checking.
So if industrial static analysis tools aren't sound, which means they produce false negatives (ie. they can pass programs with logical errors they're meant to detect), how do you use them to assure code quality?
Same way you use anything. Testing isn't perfect, yet it is still useful. Fuzzing isn't perfect, yet it is still useful. Unsound static analysis techniques aren't perfect, yet they are still useful.
The alternative is that your abstract interpretation is pinning to Top very quickly and then throwing false positives everywhere.
You can't assure code quality, you can only use them to make you code is a bit better because you fixed issues found by the tool and asymptotically approach ideal code and lower the probability there are serious errors. AKA better than nothing.
As much as I would like to nuke C and any derivative that has copy-paste compatibility with it (C++, Objective-C,...), no one is going to rewrite Linux, BSD, OpenGL, Vulkan, DirectX, Windows,macOS, iOS, Android,.... in Rust.
So I do welcome hardware memory tagging, even if isn't perfect.
Apparently Google thinks the same way, given the Android is getting hardware memory tagging as requirement on ARM, with C and C++ still having more visibility than Rust on Fuchsia.
Just like Microsoft is doing by pursuing research in Project Verona and CHERI CPU, Checked C (hiring now for the team), Visual C++ Core Guidelines static analyser, focus on .NET, instead of going full speed with Rust.
Similar story can be told about Apple's ongoing changes.
And clang's analyzer has different UI concept via web, which is far superior. And for the screen valgrind has a far superior solution. I don't see the advantage of gcc's analyzer yet. Far too verbose. and the most important errors, like wrong optimizer decisions based on their interpretation of UB code are still silenced.
gcc also has ubsan since gcc version 4.9. Many of the sanitizers are shared by the clang & gcc projects. Some functionality, like emitting errors on unsigned overflow, is confined to clang.
That's not helping. I'm talking about wrong decisions, made during compile-time optimizations, like assuming dead code or a value being NULL, and then ripping apart the written code. Without warning.
Or the famous optimized away memset call. Which is a security issue. At least a warning would be in order. Or at least an analyzer warning.
That is intrinsically limited because UB are runtime issues (otherwise they'd be compiler errors) and the compiler simply assumes they don't happen, plus many of the "UB-related" optimisations (in the sense that these optimisations change the behaviour of non-well-formed programs) are surfaced by other optimisations (largely inlining).
Problem is there are a lot of cases where the compiler doesnt know if the undefined behavior would happen in the real world. That is there is undefined behavior if some input parameter is out of range, and no way for the compiler to know that the input will always be in range - something I as a programmer with more global knowledge knows for sure which is why I don't check it.
> warning: after 3 levels of inlining (potentially across files with Link Time Optimization), some common subexpression elimination, after hoisting this thing out of a loop and proving that these 13 pointers don't alias, we found a case where you're doing something undefined. This could either be because there is a bug in your code, or because you have macros and inlining and the invalid code is dynamically unreachable but we can't prove that it is dead.
Gcc already (gcc-8) reports possible undefined behavior for loops and these are mostly out-of-bounds in my code. I like that a lot, actually, it save a ton of time.
"using the compiler the code is written in as part of the compile-edit-debug cycle, rather than having static analysis as an extra tool “on the side” (perhaps proprietary)"
Mmmm... and why not have an external tool, part of the GCC family but with a proper API, to allow to use ANY TOOL instead of bloating GCC with one more tool that won't be usable on other compilers and will need specific maintainers, althought this field is already really complex and need a lot of different knowledges ?
For example, it could be based on intermediate code so better than just source-code or machine-code analysis...
Just to be more specific: why not use the "UNIX philosophy" with a compiler to compile (translate to Intermediate Representation), an optimizer to optimize, an assembler to produce machine code from IR (with allocation registry) and so on...?
IIRC in the past GCC (or maybe just some of the maintainers?) has been resistant to that kind of architecture because it makes it easier to write proprietary extensions/plugins/backends/frontends/etc. to GCC. I'm not sure whether that has changed.
LLVM was designed to be a lot more modular, so it fits these use cases a lot better. In your example, you have the front ends (C, C++, Objective-C, Fortran frontends in LLVM proper, Rust, Zig, etc. as third-party front-ends) compiling to LLVM IR, opt for optimization, and different backends to generate machine code from IR.
Because GCC is explicitly designed to be a tangled mess (as opposed to Clang/LLVM), in part because it makes it harder for groups with different beliefs about FLOSS code to repurpose it.
Its a choice that has caused them to cede a lot of territory to Clang/LLVM.
Just a side note that the equivalent solution in LLVM/Clang is Clang Static Analyzer: https://clang-analyzer.llvm.org . But it's an external tool rather than integrating into clang
"My thinking here is that it’s best to catch problems as early as possible as the code is written, using the compiler the code is written in as part of the compile-edit-debug cycle, rather than having static analysis as an extra tool “on the side” (perhaps proprietary)."
Really? Your thinking? I mean seriously, why do you have to start off a good article and feature with a sentence like this? This is not your thinking, and if it was, you have been living under a rock for the past decades... Why the need to make it sound as if this decade long idea was yours?
I believe type sytems/type theory is likely going to be the most popular method for formal verification of programs (aka static analysis). And of course, there's a limit to what you can prove about programs (ref: Rice's theorem).
It looks great and useful. I suspect that this only works within a single translation unit and can't work between separate translation units. But maybe it could work together with lto, that would be pretty awesome.
Some of the worst lifetime issues are 3rd party library calls with unclear ownership semantics and static analyzers are just as clueless as you are. The function signature doesn't help you out in this regard (in C). My recent "favorite" is libzip's zip_open_from_source that conditionally takes ownership of its zip_source_t* argument.
Double-free's can be tracked by doing data flow analysis on the function. This is how D does it in its nascent implementation of an Ownership/Borrowing system. It can be done without DFA if getting it only 90% right and having numerous false positives is acceptable.
I've used many static checkers in the past, and the rate of false positives was high enough to dissuade me from using them. This is why D uses DFA to catch 100% of the positives with 0% negatives. I knew this could be done because the compilers were using DFA in the optimization pass.
In order to get the tracking to work, one cannot just track things for a function named "free". After all, a common thing to do is write one's own custom storage allocators, and the compiler won't know what they are. Hence, there has to be some mechanism to tell the compiler when a pointer parameter to a function is getting "consumed" by the caller, and when it is just "loaned" to the caller (hence the nomenclature of an Ownership/Borrowing system).
One of the difficulties to overcome with D in doing this is there are several complex semantic constructs that needed to be deconstructed into their component pointer operations. I noticed that Rust simplified this problem by simplifying the language :-)
But once done, it works, and works satisfyingly well.
Note that none of this is a criticism of what GCC 10 does, because the article gives insufficient detail to draw any informed conclusions. But I do see this as part of a general trend that people are sick and tired of memory safety bugs in programming languages, and it's good to see progress on all fronts here.
> This is why, for D, I was determined to use DFA to catch 100% of the positives with 0% negatives. I knew this could be done because my compilers were using DFA in the optimization pass.
Is this really true? I thought this was impossible due to Rice's theorem
Fortunately, I am unaware that it was impossible and did it anyway :-)
But it is possible I made a mistake.
It is also true that for it to work, one has to change the way one writes code, like Rust does. This is why D requires and @live attribute be added to functions to enable the checking for just those functions, so it doesn't break every program out there. It will enable incremental use of the checking at the user's option.
You're probably using a different definition of 100% than any impossibility proof would use.
Consider some code:
---
a=malloc(1);
needfree=true;
if (hashfn(first_factor(huge_static_rsanum1))&1){needfree=false;free(a);}
if (hashfn(first_factor(huge_static_rsanum2))&1){needfree=false;free(a);}
if(needfree)free(a);
---
The decision if this has a double free or not depends on the factorizations of two huge difficult to factor constants. It either double-frees or not depending on those constants.
Surely your software cannot decide that...
What you probably mean is something like "100% on real programs rather than contrived cases". Of course, in that case, your definition of 'real programs' is the catch. :P
Sometimes things that seem like they should always work except on contrived junk like the above example actually run into limitations in practice because macros and machine code generation produce ... well ... contrived junk from time to time.
I personally would want code like this flagged by static analysis. I would fix the code by not calling free in the second 'if' body if needfree was already false (just like the call at the end of the function is guarded).
I think the argument is that static analyzers don't have to work on completely unchanged code, but rather rely on humans to structure the code in a way to avoid issues.
Many years ago people regularly wrote things like "if (retval = f())" but after compilers started to complain about it people changed to write "if ((retval = f()))" instead, if they want an assignment and truthfulness testing at the same time.
Calling non-D functions means the compiler cannot check them, and will rely on the user having correctly specified and annotated the function signature.
I.e. you can have "unsafe" annotated code which the compiler doesn't check, which is indeed where the dirty deeds get swept. For example, I doubt someone could write a guaranteed safe implementation of malloc().
The idea, naturally, is to specifically mark such sections so that your crack QA team knows what to focus on, and to minimize the amount of such code.
The trick is to make the safe sections expressive enough that it is practical to write the bulk of the code in safe sections, thereby minimizing the "threat surface".
An abstract interpretation that outputs Top for all programs is sound but useless. In practice, most sound static analyses for complex problems aren't too far from that.
It's not a "negative", it's a disadvantage. "Negative" has a specific meaning that should not be used in this context.
Safe Rust is also in the same boat: it has a lot of false positives that are rejected by the borrow checker even though they would be okay, and yet it's being used just fine. Think of doubly linked lists which are pretty much impossible to implement in safe Rust unless you replace pointers with integer IDs which basically disables borrow checking. Non-lexical lifetimes are an example of downright changing the definition of the language in order to remove some of these false positives.
I didn't it that way. I read it as "downside" rather than "false negative", especially because a sound static analysis is trivial and not something to be proud of in the abstract.
"Output Top" is sound for all non-inverted lattices and takes constant time. Woohoo! But it is also useless.
I think you are both right. It's confusing because the original claim uses different terminology than usual. It said
> 100% of the positives with 0% negatives [are treated as positives]
* The "100% positives" are actual positives that show up as positive, so it's saying that there are no positives that show up as negatives i.e. "no false negatives" (even though it uses the word "positive")
* The "0% negatives" are actual negatives that show up as positives, so it's saying that there are "no false positives" (even though it uses the word "negative").
So UncleMeat's comment 'Then that doesn't mean "0% of the negatives"' and your comment 'it means you have false positives' are actually in agreement.
void main() {
check_goldbach(); // iterates over every integer > 2
// to see if it is an exception to
// the goldbach conjecture, and
// returns if so
use_after_free();
}
This program may be memory safe. It's possible that there is no exception to the goldbach conjecture, so check_goldbach will never halt, so use_after_free will never be called. It also may not be memory safe. If the goldbach conjecture is not true, check_goldbach will eventually return and then we'll call use_after_free.
You say your compiler accepts all programs which are memory safe, and rejects all that aren't. If so, you can use it to prove or disprove the goldbach conjecture. Since proving or disproving that conjecture comes with a one million dollar prize, it is surprising that you can solve it with your method
edit: I didn't mean to disparage WatlerBright's work, I only was taking issue with the idea that any method of static analysis can accept 100% of correct programs and reject 100% incorrect programs. This is an unavoidable consequence of the halting problem and being aware of it allows you to decide where you want the tradeoff to be. it sounds like his implementation has no false negatives at the cost of a few false positives that are rare enough for them not to really be an issue, which is still really cool
> You say your compiler accepts all programs which are memory safe, and rejects all that aren't.
It does it by implementing O/B rules, which force changes in the way one writes code. This may sidestep the goldbach conjecture, which I don't understand.
It is possible that the compiler simply rejects any definition of a function that has a use after free, which would both uphold the compiler's claim and also not prove or disprove the goldbach conjecture.
It'll compile because although free(p) consumes p and p is undefined immediately afterwards, p then becomes defined again via the assignment and so the while loop always enters with a defined value for p.
If that is the case then his approach has false negatives, because a function that is never called cannot introduce memory unsafety but would incorrectly be flagged as unsafe
It depends on what that means. For example, one can write perfectly correct code in a block of code marked "unsafe", it's just that the compiler cannot check it. In D, these are marked with the @system attribute.
We actually had a discussion about what to call such unsafe blocks. Other languages call them "unsafe", but I didn't care for that as it implied the blocks were actually broken. Hence we call such code "system" code.
There aren't false negatives by the design of the rules. This is different from what linters do, as linters issue warnings for code that is acceptable by the language rules.
Now you're entering a bit of a philosophical or subjective area in my opinion - I personally would want any code which is incorrect by construction to fail to compile (if possible) even if it was impossible to reach the code in question at runtime. A "false negative" like that is a feature IMO.
What Walter meant in his comment was that his static analyzer has no false positives (it never allows a memory unsafe program to compile). He's provided a few simpler examples in this thread of cases where his analyzer produces false negatives. I knew that was going to be the case because no program can flag 100% of negatives without also flagging a few positives by accident (as a consequence of Rice's theorem). I just meant to demonstrate that, but I don't know anything about D so I wanted to pick something that I was certain his analyzer would fail one way or the other.
That doesn't mean that his analyzer isn't useful. I find rust extremely useful because it catches almost me whenever I accidentally write memory unsafe code without burdening me too much otherwise. But almost every rust coder has run into a case where they wrote some code that was safe, but not allowed. That's just a fact of life and it serves no one to make incorrect claims about one's software
> I don't know anything about D so I wanted to pick something that I was certain his analyzer would fail one way or the other.
What he is talking about is a proposed implementation of the solution. It isn't actually in the D language yet. No one's tested it (except for Walter). So I would definitely take its' validity with a grain of salt.
> This is why D uses DFA to catch 100% of the positives with 0% negatives.
For example if we have a graph data structure and we are visiting it and freeing nodes, how can your static analysis know that nodes will not be visited twice by my logic and freed twice?
I think that's why you're getting the response you are in this thread - if it really did '100% of the positives with 0% negatives', it'd have to consider the logic. There's an impossibility proof for that which has already been cited in the thread. It's usually illustrated using a function that solves the halting problem rather than the Goldbach conjecture.
If the compiler rejects things that have free appear twice on branching control flow paths but aren't actually broken due to dynamic control flow (like your looping example given elsewhere) then that's a false positive, isn't it?
And people thought '0% negatives' was meaning 'no false positives'.
I see your point, and it's a valid criticism of my statement. I meant it more in the sense that the static checkers I have used would use hackish ad-hoc heuristics which did not work very well, and gets constantly tweaked by the implementor.
The D implementation, in contrast, uses a well-defined rule outlined above, and it works predictably and reliably (absent implementation bugs, rather than ad hoc rule shortcomings).
Another way of putting it is that the rules of the language are changed to make 0%/100% results workable. The compiler never says "there may be a problem here". It passes or is rejected. If it is passes, it is memory safe.
That approach is a really good point in the design space IMO. It is also the tradeoff that people have to make when designing type systems. Many programs are correct but rejected by their language's type system, but if the language is well designed it was probably a really weird and unintuitive program to begin with, so it's okay to reject it anyway.
some C compilers issue a warning for the trailing ; as do some static checkers. If the programmer intended that, the warning is a false negative because the C language rules allow it.
However, such a construct is a hard error in D. Whether you meant it or not, it is not allowed. This is what I meant.
That would be a false positive, if I am understanding things correctly. The warning is about code that is correct, yet it warns, hence false positive. If the warning was missing for incorrect code that would be a false negative. At least that is the terminilogy used for static analysis.
I think the terms normally used for this is "completeness" and "soundness", as in, the D type system is "sound" because it rejects all programs with use-after-free, but it is "incomplete" because there are some programs that cannot exhibit use-after-free for any input values, but that the type system rejects.
Given these more precise definitions, the analogous theorem would be that there is no type system (or static analysis) for use-after-free which is both sound and complete.
> I noticed that Rust simplified this problem by simplifying the language :-)
That's a bit of an open-ended qualifier. Would you say that is a positive simplification (an increase in elegance) or one that has a trade-off in reducing its expressive power?
I mentioned it as another way of solving the problem. Which way you prefer is a matter of professional taste, something I'd really prefer not diverging into in this thread.
Last time I checked - I'm not sure how long ago that is - llvm didn't detect double frees etc statically. There's an annotation framework for locking though, which I hope to play with more.
Hm. It was more recent than that. Perhaps I am just remembering that it was not possible to get it to trace user defined allocators / wrappers around malloc?
148 comments
[ 3.1 ms ] story [ 212 ms ] threadHats off to the redhat team for putting in the effort on this. Their blog posts have been really interesting. It’s definitely changing my perception of what redhat really does.
Few takeaways from that time: inter procedural matters: if your function reallocated a pointer passed as an argument, you want to treat it as ‘free’ regarding this argument, and conversely, if your function returns a newly allocated memory, you want to mark it as such, and so on. There is also a trade off between the breadth of the analysis and the human ability to comprehend it, author mentions 110 node path in the article.
The subject of my unfinished PhD thesis and something I hope also picks up is the combination of static and dynamic analysis, used iteratively. If your static analysis flags a suspicious path but does not have the means to figure out if it is true or not, instrument it and leave it to the dynamic analysis to run through it (the idea here that total instrumentation a la valgrind is detrimental to performance so you will get some gain from selective instrumentation). Conversely, dynamic analysis may provide some hints as to where static analysis should be applied at a greater depth and provide automatic annotation of functions with regard to their behaviour and - possibly - invariants, that help with the state explosion.
Running Flexelint was part of our CI chain and also part of the internal coding standard (e.g. definition of done). There was no other time in my life where I learned so much about secure coding as I did back then. Biggest challenge was agreeing about false positives and we had 1 guy in the team who maintained the official wiki document on when a lint warning needed to go on a whitelist with an agreed description of why. The initial overhead to become lint-clean got a lot of push-back but thanks to management support we got there and you could really see how things stayed at that level even after years.
It felt at times bureaucratic or like yak shaving, but in retrospect linting was what kept the code base at a quality I haven't seen ever again since. It also ensured everyone was on the same page. Taking linting seriously required a small learning curve though and lead to some discussions here or there. These discussions were really valuable since we got to really learn from another too.
When I left and went to another project it felt like a step back where we were chasing the same old bugs due to bad coding practices and it was a major step back in my career as a dev. I miss those days.
Really love that this becomes part of gcc.
Seems like mostly only GNOME Terminal and iTerm2. Here’s some that apparently won’t work:
- Konsole
- Kitty
- LXDE Terminal
- MATE Terminal
- hyper
- Windows Terminal
- ConEmu
- PuTTY
... so it’s kind of weird to suggest this is an accepted standard. Especially since some of the discussions in feature requests suggest they will likely not implement it due to security concerns or otherwise.
It isn’t like this feature degrades support for any other terminal, just improves life for some users. Why complain?
In this case it isn’t the worst problem ever. but i think support for this should probably be removed from terminal emulators unless a quorum of popular terminal emulators support it.
(Addendum: do developers actually do things that only work in virtually a single terminal emulator? Yeah. A lot of Node.JS software printed status using emoji that broke horridly on everything but macOS. It mostly works elsewhere now, and it was purely a visual problem, but I would assume many didn’t even realize what their app would’ve done in most terminal emulators. The same with hyperlinks would be a disaster.)
We shall call it the ‘terminal capabilities library’.
FWIW I am quite confident you can do better progressive feature detection in terminals, but until that somehow gains traction we’re going to get a lot of “hey, how come i cant click the link?” and the answer is they are using KDE or Windows.
Naw, that's too long, call it something short and snappy like "termcap".
This particular instance implemented by GCC10 seems the perfect example: if your terminal has no support, you get a short string like CWE-415, which is probably enough for Google; but if your terminal does support this feature, clicking on it will immediately bring you to the right page.
I always assumed the emulator accessed the working directory of the child process (as in /proc/$PID/cwd). On my terminal the CWD feature only seems to work for the topmost shell, and symlinks get resolved.
EDIT: Linked bug report mentions OCS7 (presumably an escape sequence), as one of the ways to track CWD.
https://gist.github.com/egmontkob/eb114294efbcd5adb1944c9f3c...
The problem with "not giving up at some point" is the computational complexity: Analyzing big code bases takes half an eternity (days), while using huge amounts of memory (>128GB). And once you enter the "least-defined state", you either throw lots of false positives (which gives the users a hard time) or you need to "give up" (and hence potentially miss bugs).
Disclaimer: I work for a company that builds static analysis tools. I don't see this as competition, though. Our tools are used in industries where "safety-critical" is really important - so the "giving up"-part of the analysis is no option for us, and solely relying only on GCC isn't an option for our customers either ;-)
https://www.perforce.com/products/helix-qac
The bar of zero false negatives is not useful for me when the alternative is to rely solely human code analysis and tests.
One thing I learned from using this tool is that static analyzers need to be able to configured to know about side effects of functions that are in libraries. For example, if a library function will free memory, it is important that there's a way to tell the analyzer about this behavior to avoid false positives about leaks.
Proper design, careful coding, static analysis, code review, and various forms of testing all have roles to play in delivering reliable code.
Requiring the user to add piles of annotations still sucks, even if you are smart and do something like abductive inference to identify minimally required annotations. Even something as simple as the checker framework in Java has trouble getting people to write correct annotations and has a few corner cases (what is the nullness property of a field in code reachable from a constructor, for example). Nobody does this stuff correctly for something like dataflow annotations on methods.
I've got a PhD in this and develop a static analysis tool for my job. I've never seen a productionized, fully sound tool for general purpose static analysis of general programs that solves problems more difficult that slightly augmented type checking.
The alternative is that your abstract interpretation is pinning to Top very quickly and then throwing false positives everywhere.
If all goes according to plan, I guess in a couple of decades there won't be any modern computer not making use of it.
https://msrc-blog.microsoft.com/2019/07/16/a-proactive-appro...
https://security.googleblog.com/2019/08/adopting-arm-memory-...
Lint exists since 1979.
So I do welcome hardware memory tagging, even if isn't perfect.
Apparently Google thinks the same way, given the Android is getting hardware memory tagging as requirement on ARM, with C and C++ still having more visibility than Rust on Fuchsia.
Just like Microsoft is doing by pursuing research in Project Verona and CHERI CPU, Checked C (hiring now for the team), Visual C++ Core Guidelines static analyser, focus on .NET, instead of going full speed with Rust.
Similar story can be told about Apple's ongoing changes.
And clang's analyzer has different UI concept via web, which is far superior. And for the screen valgrind has a far superior solution. I don't see the advantage of gcc's analyzer yet. Far too verbose. and the most important errors, like wrong optimizer decisions based on their interpretation of UB code are still silenced.
Or the famous optimized away memset call. Which is a security issue. At least a warning would be in order. Or at least an analyzer warning.
> warning: after 3 levels of inlining (potentially across files with Link Time Optimization), some common subexpression elimination, after hoisting this thing out of a loop and proving that these 13 pointers don't alias, we found a case where you're doing something undefined. This could either be because there is a bug in your code, or because you have macros and inlining and the invalid code is dynamically unreachable but we can't prove that it is dead.
Mmmm... and why not have an external tool, part of the GCC family but with a proper API, to allow to use ANY TOOL instead of bloating GCC with one more tool that won't be usable on other compilers and will need specific maintainers, althought this field is already really complex and need a lot of different knowledges ?
For example, it could be based on intermediate code so better than just source-code or machine-code analysis...
LLVM was designed to be a lot more modular, so it fits these use cases a lot better. In your example, you have the front ends (C, C++, Objective-C, Fortran frontends in LLVM proper, Rust, Zig, etc. as third-party front-ends) compiling to LLVM IR, opt for optimization, and different backends to generate machine code from IR.
Its a choice that has caused them to cede a lot of territory to Clang/LLVM.
https://lists.gnu.org/archive/html/emacs-devel/2015-02/msg00...
Really? Your thinking? I mean seriously, why do you have to start off a good article and feature with a sentence like this? This is not your thinking, and if it was, you have been living under a rock for the past decades... Why the need to make it sound as if this decade long idea was yours?
Difference is, their idea came to fruition, and their idea has contributed to what is arguably the world's most important piece of software
Some of the worst lifetime issues are 3rd party library calls with unclear ownership semantics and static analyzers are just as clueless as you are. The function signature doesn't help you out in this regard (in C). My recent "favorite" is libzip's zip_open_from_source that conditionally takes ownership of its zip_source_t* argument.
https://libzip.org/documentation/zip_open_from_source.html
https://libzip.org/documentation/zip_source_free.html
I've used many static checkers in the past, and the rate of false positives was high enough to dissuade me from using them. This is why D uses DFA to catch 100% of the positives with 0% negatives. I knew this could be done because the compilers were using DFA in the optimization pass.
In order to get the tracking to work, one cannot just track things for a function named "free". After all, a common thing to do is write one's own custom storage allocators, and the compiler won't know what they are. Hence, there has to be some mechanism to tell the compiler when a pointer parameter to a function is getting "consumed" by the caller, and when it is just "loaned" to the caller (hence the nomenclature of an Ownership/Borrowing system).
One of the difficulties to overcome with D in doing this is there are several complex semantic constructs that needed to be deconstructed into their component pointer operations. I noticed that Rust simplified this problem by simplifying the language :-)
But once done, it works, and works satisfyingly well.
Note that none of this is a criticism of what GCC 10 does, because the article gives insufficient detail to draw any informed conclusions. But I do see this as part of a general trend that people are sick and tired of memory safety bugs in programming languages, and it's good to see progress on all fronts here.
Is this really true? I thought this was impossible due to Rice's theorem
But it is possible I made a mistake.
It is also true that for it to work, one has to change the way one writes code, like Rust does. This is why D requires and @live attribute be added to functions to enable the checking for just those functions, so it doesn't break every program out there. It will enable incremental use of the checking at the user's option.
Consider some code:
---
a=malloc(1);
needfree=true;
if (hashfn(first_factor(huge_static_rsanum1))&1){needfree=false;free(a);}
if (hashfn(first_factor(huge_static_rsanum2))&1){needfree=false;free(a);}
if(needfree)free(a);
---
The decision if this has a double free or not depends on the factorizations of two huge difficult to factor constants. It either double-frees or not depending on those constants.
Surely your software cannot decide that...
What you probably mean is something like "100% on real programs rather than contrived cases". Of course, in that case, your definition of 'real programs' is the catch. :P
Sometimes things that seem like they should always work except on contrived junk like the above example actually run into limitations in practice because macros and machine code generation produce ... well ... contrived junk from time to time.
Many years ago people regularly wrote things like "if (retval = f())" but after compilers started to complain about it people changed to write "if ((retval = f()))" instead, if they want an assignment and truthfulness testing at the same time.
The D implementation would reject such code. The DFA assumes all control paths are executed. For example,
is rejected as use-after-free. is also rejected as use-after-free. If the DFA is done properly, you will not be able to trick it.I think this is just moving potential problem under rug, which is best it can do, given Rice Theorem
I.e. you can have "unsafe" annotated code which the compiler doesn't check, which is indeed where the dirty deeds get swept. For example, I doubt someone could write a guaranteed safe implementation of malloc().
The idea, naturally, is to specifically mark such sections so that your crack QA team knows what to focus on, and to minimize the amount of such code.
The trick is to make the safe sections expressive enough that it is practical to write the bulk of the code in safe sections, thereby minimizing the "threat surface".
An abstract interpretation that outputs Top for all programs is sound but useless. In practice, most sound static analyses for complex problems aren't too far from that.
Safe Rust is also in the same boat: it has a lot of false positives that are rejected by the borrow checker even though they would be okay, and yet it's being used just fine. Think of doubly linked lists which are pretty much impossible to implement in safe Rust unless you replace pointers with integer IDs which basically disables borrow checking. Non-lexical lifetimes are an example of downright changing the definition of the language in order to remove some of these false positives.
"Output Top" is sound for all non-inverted lattices and takes constant time. Woohoo! But it is also useless.
> 100% of the positives with 0% negatives [are treated as positives]
* The "100% positives" are actual positives that show up as positive, so it's saying that there are no positives that show up as negatives i.e. "no false negatives" (even though it uses the word "positive")
* The "0% negatives" are actual negatives that show up as positives, so it's saying that there are "no false positives" (even though it uses the word "negative").
So UncleMeat's comment 'Then that doesn't mean "0% of the negatives"' and your comment 'it means you have false positives' are actually in agreement.
You say your compiler accepts all programs which are memory safe, and rejects all that aren't. If so, you can use it to prove or disprove the goldbach conjecture. Since proving or disproving that conjecture comes with a one million dollar prize, it is surprising that you can solve it with your method
edit: I didn't mean to disparage WatlerBright's work, I only was taking issue with the idea that any method of static analysis can accept 100% of correct programs and reject 100% incorrect programs. This is an unavoidable consequence of the halting problem and being aware of it allows you to decide where you want the tradeoff to be. it sounds like his implementation has no false negatives at the cost of a few false positives that are rare enough for them not to really be an issue, which is still really cool
It does it by implementing O/B rules, which force changes in the way one writes code. This may sidestep the goldbach conjecture, which I don't understand.
Clearly.
https://news.ycombinator.com/newsguidelines.html
It depends on what that means. For example, one can write perfectly correct code in a block of code marked "unsafe", it's just that the compiler cannot check it. In D, these are marked with the @system attribute.
We actually had a discussion about what to call such unsafe blocks. Other languages call them "unsafe", but I didn't care for that as it implied the blocks were actually broken. Hence we call such code "system" code.
There aren't false negatives by the design of the rules. This is different from what linters do, as linters issue warnings for code that is acceptable by the language rules.
Climbing a ladder on a table is unsafe. Does that imply the ladder or table is broken? No.
how is your comment, under any reasonable interpretation of what Walter wrote, not pointless pedantry?
That doesn't mean that his analyzer isn't useful. I find rust extremely useful because it catches almost me whenever I accidentally write memory unsafe code without burdening me too much otherwise. But almost every rust coder has run into a case where they wrote some code that was safe, but not allowed. That's just a fact of life and it serves no one to make incorrect claims about one's software
What he is talking about is a proposed implementation of the solution. It isn't actually in the D language yet. No one's tested it (except for Walter). So I would definitely take its' validity with a grain of salt.
It is in the released compiler as a preview feature.
Those would be false negatives, not false positives. FP = flagging what should not be flagged, FN = not flagging what should be flagged.
For example if we have a graph data structure and we are visiting it and freeing nodes, how can your static analysis know that nodes will not be visited twice by my logic and freed twice?
If the compiler rejects things that have free appear twice on branching control flow paths but aren't actually broken due to dynamic control flow (like your looping example given elsewhere) then that's a false positive, isn't it?
And people thought '0% negatives' was meaning 'no false positives'.
The D implementation, in contrast, uses a well-defined rule outlined above, and it works predictably and reliably (absent implementation bugs, rather than ad hoc rule shortcomings).
Another way of putting it is that the rules of the language are changed to make 0%/100% results workable. The compiler never says "there may be a problem here". It passes or is rejected. If it is passes, it is memory safe.
However, such a construct is a hard error in D. Whether you meant it or not, it is not allowed. This is what I meant.
A construct in D that would pass is:
Given these more precise definitions, the analogous theorem would be that there is no type system (or static analysis) for use-after-free which is both sound and complete.
That's a bit of an open-ended qualifier. Would you say that is a positive simplification (an increase in elegance) or one that has a trade-off in reducing its expressive power?