7 ms·

Your example does not pass the verifier cbmc /tmp/walter.c --bounds-check --pointer-check --function test ... [get.pointer_dereference.5] line 3 dere

Your example does not pass the verifier cbmc /tmp/walter.c --bounds-check --pointer-check --function test ... [get.pointer_dereference.5] line 3 dereference failure: pointer outside object bounds in buffer[(signed long int)10]: FAILURE ... There are many footguns. People love their guns. Makes them feel powerful.

WalterBright 3y ago
int get(char* buffer, int i) { return buffer[i]; } #include <stdio.h> void test() { char buffer[10]; get(buffer, getc(stdin)); }
- nanolith 3y ago
  CBMC's default contract for getc returns a non-deterministic integer value. A non-deterministic integer value basically counts as "pick a value that would cause this de-reference to crash the machine model". So, it will find a counter-example.
  - philzook 3y ago
    Yes, it returned the same "FAILURE" along with a couple new checks about getc that do pass.
    - WalterBright 3y ago
      Sounds like it's doing a solid job of data flow analysis. But I can still produce cases where it cannot determine either the range of the index or the length of the array being pointed to. The programmer will have to add code to keep track of the length of the array, and add code to check the value of the index. The good thing is the analyzer will tell you where you'll need to add those checks. With the proposal I made, none of this is necessary. It just works. Over two decades of experience with this approach in D is it-just-works.
      - nanolith 3y ago
        I'm curious, have you used CBMC? The machine model tracks the array with its size and compares this to any index. This is loaded into an SMT solver. This is not a standard static analyzer. It's compiling the code to an abstract machine model and then running through this model with an SMT solver. CBMC isn't perfect, but the strategies you are talking about are meant to defeat a linter or a shallow analyzer in a compiler. CBMC isn't a linter.
        WalterBright 3y ago
        I have never heard of CBMC before this thread. SMT cannot solve cases where it simply cannot know what the length of an array is. For example, when array is allocated in code not available to the solver, or is set by the environment. I remember trying out Spark a few years ago, which advertised its compile time checking abilities. I tried using an integer equation that used an OR, and it gave up on it. If you need to add in range checking code to help the solver along, then the range check itself is a source of bugs, and the range limit has to be made available somewhere and be correct. In my proposal, the array length is set at the time of creation of the array, and the length is carried along with the pointer. The solver's role then becomes one of eliminating the bounds check in the cases where it can prove the index is within range. The user doesn't have to do anything. We've been using it in the implementation of the D compiler for a very long time now, and problems with buffer overflows are a faded memory. P.S. I also added manual integer overflow checks when passing the size to malloc(), no matter how unlikely an overflow would be :-)
        nanolith 3y ago
        > SMT cannot solve cases where it simply cannot know what the length of an array is. Sure it can. It sets the array length to a non-deterministic unsigned integer, and then finds a counter-example where this array length is invalid. CBMC will also make the array pointer itself non-deterministic if you haven't refined it. So, the pointer could be NULL, could be pointing to invalid memory, etc. Don't think of values as fixed numbers, but rather as functions shaping a non-deterministic value. The range check made upstream becomes part of this function. The goal of the SMT solver is to find a counter-example that crashes the machine model. If you want a rather leaky abstraction, imagine that by transforming the source code into an SMT equation, it's effectively turning it inside out and transforming it into a logic equation with modulo math. I agree with you that it would be nice if bounds were included in C arrays. But, we have to work with what we have. Unfortunately, especially in firmware that requires a commercial C compiler, we are stuck with C. In those cases, if we want safer software, we need tooling like this.
- mhh__ 3y ago
  A lot of static analysis tools explicitly support forcing you to check the value of "tainted" values such as return values of getc and so on i.e. even with slices you want to be able to catch this kind of thing ahead of time.
Joker_vD 3y ago
> There are many footguns. People love their guns. Makes them feel powerful. Well, duh: if you remove the most egregious footguns from C, you end up basically with Pascal, and here is Why Pascal Is Not My Favorite Programming Language. And when you try to explain to them that C's abstract machine has semantics of "when you omit a safety check, you actually makes a promise to the compiler that this check is redundant, that you'll promise that you'll make sure in some other way that in no possible execution will the illegal values ever show up in this place, and the compiler will actually hold you to this promise" — they throw tantrums and try to argue that no, it hasn't this semantics, and even if has, it's not the semantics as originally intended by K&R and it is the authors of the C compilers who are wrong (even though the authors of C compilers are the people who actually write both the C standards and the C compilers...) Must have to do something with imprintment: I've learned C as my 3rd language, and from the start I was taught that its UB is absolutely insane — and I've never felt "nah, it should just do what I meant, dangit" denial about it, only "this is sad, how can I even know while writing code when I am making a baseless promise especially when it's made by omitting something?" But like you've said, people like their footguns.
- GuestHNUser 3y ago
  > Must have to do something with imprintment Eh, I think most C programmers frustrations with UB stem from knowing that the C standard has fundamental flaws and modern compilers abuse that fact for "optimizations" on UB. This paper covers the topic pretty well[0]. I fully support Casey Muratori's viewpoint that undefined behavior should not exist in the standard[1]. Instead, the C standard should enumerate all valid behaviors compliant compilers can implement. This would allow compilers to make unintuitive optimizations for the platforms that need them, but still allow programmers to be certain that their program semantics will not change in different versions of the said compiler. [0] https://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_2015_submission_29.pdf https://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_20... [1] https://youtu.be/dyI0CwK386E?si=vsqJ8uWHY8xkGmFm https://youtu.be/dyI0CwK386E?si=vsqJ8uWHY8xkGmFm
  - Joker_vD 3y ago
    > I think most C programmers frustrations with UB stem from knowing that the C standard has fundamental flaws and modern compilers abuse that fact for "optimizations" on UB Do they actually know that? I don't think so. Let's take [0] for instance (the author is an expreienced C programmer who loves the language and wrote a re-implementation of bc in it): There seemed to be a lot of misunderstandings; I could not get a handle on what this person thought UB meant. I finally figured it out: this person’s definition of UB was not “the language spec can’t guarantee anything.” Instead, it was “compilers can assume UB does not exist and optimize accordingly.” Wat. Yep. Apparently, that was news to him, even though C implementations have been behaving like that for about 30 years already, and you can read the rest of the post for the "this is evil, we the users must do something about it" take. And the proposed "something" is not "we should instead use a language with actually defined semantics", oh no. It's "use compiler flags to force more reasonable behaviour, hopefully" and "somebody should write boringcc, unfortunately, I am myself a bit too busy for that". Well, despite numerous pleas and several attempts, nobody has managed to write boringcc which is telling of something, I'm just not sure of what exactly. So... I think it is about imprinting: "Oh, it's a wonderful language, well, it would be if it was actually implemented the way I used to think it is implemented (and I still think it should be implemented that way) but still, it's a wonderful language if only not for that pesky realitiy" is forcing unfounded expectations onto reality, and where do these expectations even come from in the first place? And yeah, I fully agree with you that C standard should've probably done that. But it didn't happen, and it can't happen because backwards compatibility [1]. But even then, C programs would still be non-portable, in a sense that you have to use #ifdef's for tinkering with platform-specific behaviour for anything interesting, because C standard even today leaves a lot of stuff completely up to implementation, see [2] for an especially apalling example, even without touching UB. [0] https://gavinhoward.com/2023/08/the-scourge-of-00ub/ https://gavinhoward.com/2023/08/the-scourge-of-00ub/ [1] https://thephd.dev/your-c-compiler-and-standard-library-will-not-help-you https://thephd.dev/your-c-compiler-and-standard-library-will... [2] https://thephd.dev/conformance-should-mean-something-fputc-and-freestanding https://thephd.dev/conformance-should-mean-something-fputc-a...

WalterBright 3y ago

int get(char* buffer, int i) { return buffer[i]; } #include <stdio.h> void test() { char buffer[10]; get(buffer, getc(stdin)); }

nanolith 3y ago
CBMC's default contract for getc returns a non-deterministic integer value. A non-deterministic integer value basically counts as "pick a value that would cause this de-reference to crash the machine model". So, it will find a counter-example.
- philzook 3y ago
  Yes, it returned the same "FAILURE" along with a couple new checks about getc that do pass.
  - WalterBright 3y ago
    Sounds like it's doing a solid job of data flow analysis. But I can still produce cases where it cannot determine either the range of the index or the length of the array being pointed to. The programmer will have to add code to keep track of the length of the array, and add code to check the value of the index. The good thing is the analyzer will tell you where you'll need to add those checks. With the proposal I made, none of this is necessary. It just works. Over two decades of experience with this approach in D is it-just-works.
    - nanolith 3y ago
      I'm curious, have you used CBMC? The machine model tracks the array with its size and compares this to any index. This is loaded into an SMT solver. This is not a standard static analyzer. It's compiling the code to an abstract machine model and then running through this model with an SMT solver. CBMC isn't perfect, but the strategies you are talking about are meant to defeat a linter or a shallow analyzer in a compiler. CBMC isn't a linter.
      - WalterBright 3y ago
        I have never heard of CBMC before this thread. SMT cannot solve cases where it simply cannot know what the length of an array is. For example, when array is allocated in code not available to the solver, or is set by the environment. I remember trying out Spark a few years ago, which advertised its compile time checking abilities. I tried using an integer equation that used an OR, and it gave up on it. If you need to add in range checking code to help the solver along, then the range check itself is a source of bugs, and the range limit has to be made available somewhere and be correct. In my proposal, the array length is set at the time of creation of the array, and the length is carried along with the pointer. The solver's role then becomes one of eliminating the bounds check in the cases where it can prove the index is within range. The user doesn't have to do anything. We've been using it in the implementation of the D compiler for a very long time now, and problems with buffer overflows are a faded memory. P.S. I also added manual integer overflow checks when passing the size to malloc(), no matter how unlikely an overflow would be :-)
        nanolith 3y ago
        > SMT cannot solve cases where it simply cannot know what the length of an array is. Sure it can. It sets the array length to a non-deterministic unsigned integer, and then finds a counter-example where this array length is invalid. CBMC will also make the array pointer itself non-deterministic if you haven't refined it. So, the pointer could be NULL, could be pointing to invalid memory, etc. Don't think of values as fixed numbers, but rather as functions shaping a non-deterministic value. The range check made upstream becomes part of this function. The goal of the SMT solver is to find a counter-example that crashes the machine model. If you want a rather leaky abstraction, imagine that by transforming the source code into an SMT equation, it's effectively turning it inside out and transforming it into a logic equation with modulo math. I agree with you that it would be nice if bounds were included in C arrays. But, we have to work with what we have. Unfortunately, especially in firmware that requires a commercial C compiler, we are stuck with C. In those cases, if we want safer software, we need tooling like this.
mhh__ 3y ago
A lot of static analysis tools explicitly support forcing you to check the value of "tainted" values such as return values of getc and so on i.e. even with slices you want to be able to catch this kind of thing ahead of time.

Joker_vD 3y ago

> There are many footguns. People love their guns. Makes them feel powerful. Well, duh: if you remove the most egregious footguns from C, you end up basically with Pascal, and here is Why Pascal Is Not My Favorite Programming Language. And when you try to explain to them that C's abstract machine has semantics of "when you omit a safety check, you actually makes a promise to the compiler that this check is redundant, that you'll promise that you'll make sure in some other way that in no possible execution will the illegal values ever show up in this place, and the compiler will actually hold you to this promise" — they throw tantrums and try to argue that no, it hasn't this semantics, and even if has, it's not the semantics as originally intended by K&R and it is the authors of the C compilers who are wrong (even though the authors of C compilers are the people who actually write both the C standards and the C compilers...) Must have to do something with imprintment: I've learned C as my 3rd language, and from the start I was taught that its UB is absolutely insane — and I've never felt "nah, it should just do what I meant, dangit" denial about it, only "this is sad, how can I even know while writing code when I am making a baseless promise especially when it's made by omitting something?" But like you've said, people like their footguns.

GuestHNUser 3y ago
> Must have to do something with imprintment Eh, I think most C programmers frustrations with UB stem from knowing that the C standard has fundamental flaws and modern compilers abuse that fact for "optimizations" on UB. This paper covers the topic pretty well[0]. I fully support Casey Muratori's viewpoint that undefined behavior should not exist in the standard[1]. Instead, the C standard should enumerate all valid behaviors compliant compilers can implement. This would allow compilers to make unintuitive optimizations for the platforms that need them, but still allow programmers to be certain that their program semantics will not change in different versions of the said compiler. [0] https://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_2015_submission_29.pdf https://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_20... [1] https://youtu.be/dyI0CwK386E?si=vsqJ8uWHY8xkGmFm https://youtu.be/dyI0CwK386E?si=vsqJ8uWHY8xkGmFm
- Joker_vD 3y ago
  > I think most C programmers frustrations with UB stem from knowing that the C standard has fundamental flaws and modern compilers abuse that fact for "optimizations" on UB Do they actually know that? I don't think so. Let's take [0] for instance (the author is an expreienced C programmer who loves the language and wrote a re-implementation of bc in it): There seemed to be a lot of misunderstandings; I could not get a handle on what this person thought UB meant. I finally figured it out: this person’s definition of UB was not “the language spec can’t guarantee anything.” Instead, it was “compilers can assume UB does not exist and optimize accordingly.” Wat. Yep. Apparently, that was news to him, even though C implementations have been behaving like that for about 30 years already, and you can read the rest of the post for the "this is evil, we the users must do something about it" take. And the proposed "something" is not "we should instead use a language with actually defined semantics", oh no. It's "use compiler flags to force more reasonable behaviour, hopefully" and "somebody should write boringcc, unfortunately, I am myself a bit too busy for that". Well, despite numerous pleas and several attempts, nobody has managed to write boringcc which is telling of something, I'm just not sure of what exactly. So... I think it is about imprinting: "Oh, it's a wonderful language, well, it would be if it was actually implemented the way I used to think it is implemented (and I still think it should be implemented that way) but still, it's a wonderful language if only not for that pesky realitiy" is forcing unfounded expectations onto reality, and where do these expectations even come from in the first place? And yeah, I fully agree with you that C standard should've probably done that. But it didn't happen, and it can't happen because backwards compatibility [1]. But even then, C programs would still be non-portable, in a sense that you have to use #ifdef's for tinkering with platform-specific behaviour for anything interesting, because C standard even today leaves a lot of stuff completely up to implementation, see [2] for an especially apalling example, even without touching UB. [0] https://gavinhoward.com/2023/08/the-scourge-of-00ub/ https://gavinhoward.com/2023/08/the-scourge-of-00ub/ [1] https://thephd.dev/your-c-compiler-and-standard-library-will-not-help-you https://thephd.dev/your-c-compiler-and-standard-library-will... [2] https://thephd.dev/conformance-should-mean-something-fputc-and-freestanding https://thephd.dev/conformance-should-mean-something-fputc-a...