No engine can be 100% perfect of course, the original comment is broadly accurate though. CodeQL builds a full semantic database including types and dataflow from source code, then runs queries against that. QL is fundamentally a logic programming language that is only concerned with the satisfiably of the given constraint.
If dataflow is not provably connected from source to sink, an alert is impossible. If a sanitization step interrupts the flow of potentially tainted data, the alert is similarly discarded.
The end-to-end precision of the detection depends on the queries executed, the models of the libraries used in the code (to e.g., recognize the correct sanitizers), and other parameters. All of this is customizable by users.
All that can be overwhelming though, so we aim to provide sane defaults. On GitHub, you can choose between a "Default" and "Extended" suite. Those are tuned for different levels of potential FN/FP based on the precision of the query and severity of the alert.
Severities are calculated based on the weaknesses the query covers, and the real CVE these have caused in prior disclosed vulnerabilities.
Sorry, I don’t understand the point you’re making. If CodeQL reports that you have a XSS vulnerability in your code, and its report includes the complete and specific code path that creates that vulnerability, how is Rice’s theorem applicable here? We’re not talking about decidability of some semantic property in the general case; we’re talking about a specific claim about specific code that is demonstrably true.
> We’re not talking about decidability of some semantic property in the general case; we’re talking about a specific claim about specific code
Is CodeQL special cased for your code? I very much doubt that. Then it must work in the general case. At that point decidability is impossible and at best either false positives or false negatives can be guaranteed to be absent, but not both (possibly neither of them!)
I don't doubt CodeQL claims can be demonstrably true, that's still coherent with Rice's theorem. However it does mean you'll have false negatives, that is cases where CodeQL reports no provable claim while your code is vulnerable to some issues.
OK, but all I said before was that CodeQL’s approach where it supplies a specific example to support a specific problem report is inherently resistant to false positives.
Clearly it is still possible to generate a false positive if, for example, CodeQL’s algorithm thinks it has found a path through the code where unsanitised user data can be used dangerously, but in fact there was a sanitisation step along the way that it didn’t recognise. This is the kind of situation where the theoretical result about not being able to determine whether a semantic property holds in all cases is felt in practical terms.
It still seems much less likely that an algorithm that needs to produce a specific demonstration of the problem it claims to have found will result in a false positive than the kind of naïve algorithms we were discussing before that are based on a generic look-up table of software+version=vulnerability without any attempt to determine whether there is actually a path to exploit that vulnerability in the real code.
Rice’s theorem applies to any non-trivial semantic property.
Looking at the docs, I’m not really sure CodeQL is semantic in the same sense as Rices theorem. It looks syntactic more than semantic.
Eg breaking Rices theorem would require it to detect that an application isn’t vulnerable if it contains the vulnerability but only in paths that are unreachable. Like
if request.params.limit > 1000:
throw error
# 1000 lines of code
if request.params.limit > 1000:
call_vulnerable_code()
I’m not at a PC right now, but I’d be curious if CodeQL thinks that’s vulnerable or not.
It’s probably demonstrably true that there is syntactically a path to the vulnerability, I’m a little dubious that it’s demonstrably true the code path is actually reachable without executing the code.
In light of that, I am wondering why the article opted to go for "However, determining the optimal join order is far from trivial.", when there are hard results in literature.
I was also missing mentioning "sideways information passing", though some of methods are exactly that.
I am wondering whether the company consults literature or whether they fiddle about, mostly reinventing the wheel.
While tedious, you can do the rewrite block-wise from the insertion point and only store a an additional block's worth of the rest (or twice as much as you inserted)
ABCDE, to insert 1 after C: store D, overwrite D with 1, store E, overwrite E with D, write E.
From TFA and AndyP's slides it seems to specifically refer to a variant of SSO where, for large strings, a fixed-sized prefix of the string is stored along-side the pointer, in the same location as that fixed-size prefix would be fore SSO strings. This means that strings lacking a common prefix can be quickly compared without pointer-chasing (or even knowing if they are small vs large).
I had a lot of contact with computer science students coming from the other side, meaning they used Z3 or other (SMT) solvers as blackboxes which they just use at a certain point in their algorithm without having thought what theories they are using (the T in SMT) and what's undecidable in general or in that theory.
So I had quite a few "groundbreaking" approaches end in disappointment.
It's important to know the capabilities and limits of your tools.
I'm not a rust or systems programmer but I think it meant that as an ABI or foreign function interface bitfields are not stable or not intuitive to use, as they can't be declared granularily enough.
C's bit-fields ABI isn't great either. In particular, the order of allocation of bit-fields within a unit and alignment of non-bit-field structure members are implementation defined (6.7.2.1). And bit-fields of types other than `_Bool`, `signed int` and `unsigned int` are extensions to the standard, so that somewhat limits what types can have bitfields.
I think core of the problem in property-based testing that the property/specification needs to be quite simple compared to the implementation.
I did some property-based testing in Haskell and in some cases the implementation was the specification verbatum. So what properties should I test?
It was clearer where my function should be symmetric in the arguments or that there is a neutral element, etc..
If the property is basically your specification which (as the language is very expressive) is your implementation then you're just going in circles.
Yeah, reimplementing the solution just to have something to check against is a bad idea.
I find that most tutorials talk about "properties of function `foo`", whereas I prefer to think about "how is function `foo` related to other functions". Those relationships can be expressed as code, by plugging outputs of one function into arguments of another, or by sequencing calls in a particular order, etc. and ultimately making assertions. However, there will usually be gaps; filling in those gaps is what a property's inputs are for.
Another good source of properties is trying to think of ways to change an expression/block which are irrelevant. For example, when we perform a deletion, any edits made beforehand should be irrelevant; boom, that's a property. If something would filter out negative values, then it's a property that sprinkling negative values all over the place has no effect. And so on.
The range can be a product type, as can the domain. Most languages are expressive enough that you can create the product type (struct). You're right on point.
> valuing where papers are published over what they contribute
And who is the arbiter of that? This is an imperfect but easy shorthand. Like valuing grades and degrees instead of what people actually took away from school.
In an ideal world we would see all this intangible worth in people's contributions. But we don't have time for that.
So the PhD committee decides on exactly that measure whether there are enough published articles for a cumulative dissertation and if that's enough. What's exactly the alternative? Calling in fresh reviews to weigh the contributions?
Avoiding the problem altogether is just throwing up your hands and saying "this is too hard so I'm not going to even try".
We already know there is some way to do it because researchers do salami slicing where they take one paper and split it up into multiple papers to get more numbers, out of the same work. Therefore one might for example look at a paper and think, how many papers could one get out of this if they were to take part in salami slicing in order to get at-least some measure of this initially.
By Rice's Theorem, I somehow doubt that.