NVIDIA Security Team: 'What if We Just Stopped Using C?' - Slashdot

Posted by EditorDavid

• ›

  Where expertise is devalued, doom follows. Mark my words.

  • Re:

    "The determined programmer can write buggy code in any language".

    They should just switch to Haskell. Someone, and that somone would be an academic, once tried to tell me that it's impossible to write incorrect code in Haskell.

    • Re:

      It is also impossible to write useful code in Haskell;)
      well, practically impossible.

    • Re: What if, indeed.

      The grain of truth in that lie is that given a language with a strict and expressive type system (like Haskell or Scala) and a tradition for using it properly (unlike Java and c#), it's just much harder to write incorrect code. It reduces the set of incorrect programs that would compile by a huge factor, and leaves you with a lot less code to verify.

      • Re:

        I estimate that about 90% of the bugs in my code are mistakes that could happen in any language. Stuff like array overruns or stack corruption are relatively rare. As your project gets more and more complicated, mistakes happen at higher and higher levels, and language isn't going to help you.

        • Re: What if, indeed.

          I agree with that. Most bugs hide in the diff between reality and the developer's understanding of it. Still even with that it really helps to use a language that lets you encode intent. Makes it more likely that kind of error is caught in code review.

          • Re: What if, indeed.

            You can encode intent in C++. You can also write terrible spaghetti code. It's all about how you use it.

        • Re:

          It does, or your modern computer could never ever be built. All the digital logic in a CPU, GPU, chipset etc is written as code in one flavor of HDL or another. Except it pretty much has to work the first time, there is no patching it after it's already in silicon. So how is it done? Formal verification is the answer.

    • As someone who programmed a lot of C++ and Haskell, the languages are similar in a strange way. The only difference is in what's easy and what's hard. In Haskell, all the standard library is full with super safe and friendly containers. In C++, it is full with pointers and APIs with bound checking.

      Now comes the interesting part. Theoretically, C++ allows you to write completely safe containers if you always bounds checking apis and rely on ugly templates. Haskell also allows you to directly access memory, do mallocs, and violate access.

      The only difference is in the defaults of both languages and what functionality they choose to hide behind complicated APIs.

      I think both languages have their places. In industry projects I'm maintaining now, some would better remain in C++ while others should have been rewritten in Haskell.

  • Re:

    Expertise is not being devalued.

    And no, you are not smart enough to write secure code in C.

  • • • Re: What if, indeed.

        Both the racism of the past and the racism of the present are bad.

        
        
        And you cannot solve racism with more and different racism. You solve it by letting humans make free will choices and discovering that equality is far and away the optimal solution.

      • • • Re:

            LOL! Thank you for exquisitely proving my point. The law says you can't discriminate against someone because of the color ot their skin, yet it many cases that is the deciding factor whether to hire someone. The same with a person's name. If it has a "white" bias to it, the person is statistically more likely to be hired [wbur.org]. I've seen people post they will never hire a woman for a job. Surely you'll be just as "outraged" at that, right?

            Here's one for you. A black couple went to sell their home. They recei

            • • Re:

                LOL

                Now join me in condemning the PROVEN anti-man hiring practices of American universities. - You shouted a load of crap there and you didn't "prove" anything with sourcing.

                Join me in demanding a stop to the teaching of manhate under the guise of "Wimmins Studies". - Let me guess, you're some less-than-mediocre racial supremacist incel with delusions of adequacy.

      • • Re: What if, indeed.

          I agree neutrality is best, but blind doesn't work. We have a multitude of evidence on that. This is why affirmative action is so important; it's the measuring stick by which we can verify neutrality.

          • Re: measuring stick

            Go read Harrison Bergeron.
            The possibility thatball races are precisely the same on average as other races is just one of thousands. A quick look at competitive sports teams doesn't support it. Sure there will be many overlapping individuals, but racial equity is at odds with equality. 'Equity' is just codified plundering of others based on race. 'Our team/race' has got to get it's slice as a group even if then individuals don't merit it.
            There is nothing wrong with that point of view, but faced with a te

    • • Re:

        I didn't express any thoughts on the policy. I merely linked a study that demonstrated racism and sexism in hiring that exists today. And then I made a point that if your problem is discrimination in hiring, then surely naked in-your-face discrimination because some people are just born with wrong skin tone and genitalia is far worse than whatever we're talking about in the topic.

• proof (Score:3, Interesting)

  by Artenzio ( 10222659 ) on Sunday November 13, 2022 @03:41AM (#63046969)

  Fortunately, it is possible to prove mathematically that your code behaves in precise accordance with its specification.

  I'll give you a program, and a specification that says "this program halts"

  • by ShanghaiBill ( 739463 ) on Sunday November 13, 2022 @04:07AM (#63047005)

    I'll give you a program, and a specification that says "this program halts"

    The halting problem [wikipedia.org] says that you can't prove that any program halts or not.

    But you can prove the behavior of programs that are specifically written to be proven, including whether or not they halt.

    In practice, those programs tend to be trivial, and proofs of correctness are not very useful.

    • Re:

      In practice, about 30 years ago, when I was still a student, there were already formally verified compilers and at least one formally verified operating system. This is everything else than trivial.

      • Re:

        So in 1992, there was a proven correct OS with zero bugs that never ever crashed? Citation needed.

        • Re: proof

          My random guess is they're thinking of QNX which was famous at the time for running nuclear plants and other high reliability situations for years without reboots and being able to upgrade modules in place. The kernel had very few calls which would make it easier to vet.

          • by ShanghaiBill ( 739463 ) on Sunday November 13, 2022 @07:21AM (#63047283)

            My random guess is they're thinking of QNX

            QNX is a microkernel, so most functionality is implemented outside the kernel. It is easy to do things reliably when you don't do much of anything. But the QNX Wikipedia page [wikipedia.org] says nothing about formal verification, and a Google search brings up nothing.

            The L4 microkernel [wikipedia.org], written in Haskell, was supposedly formally verified in the late 1990s.

            • Re:

              Not only supposedly, I was in the same operating system group at TU Dresden, Germany, which formally verified it.

              • Re:

                PS: L4 at first was written in i486 assembler and later at TU Dresden reimplemented in C++, calling their version Fiasco. Other implementations are Pistacchio and seL4.

            • Re: proof

              RTEMS, QNX, PikeOS, etc. There are a few safety certified operating systems used by trains, cranes, mining trucks etc.

      • Re:

        The "formally verified operating system" was probably just the microkernel.

        A huge problem with operating systems is that they have to deal with physical hardware which is typically riddled with hardware bugs and undocumented behavior that has to be worked around. Good luck proving anything.

    • Re:

      "The halting problem [wikipedia.org] says that you can't prove that any program halts or not."

      No. The program "HALT" provably halts. The program "while (true) {}" does not. What you cannot prove is that an arbitrary one "halts or not". "Any" particular program may be provable or may not me.

      "But you can prove the behavior of programs that are specifically written to be proven, including whether or not they halt."

      This is in open contradiction to your previous claim. "Any" program includes programs "speci

    • Re:

      For the vast majority of programs, it's obvious whether they halt or not. Generally programs are set up in a giant loop of some sort, and when you encounter that, you can show that it doesn't halt (or in which cases it halts). This is useful, because in practice you want to know in which cases your program halts.

      Most practical code is not self-referential, it's not even recursive. So the approach is to look for any strange for loops that might be infinite loops. Once you've analyzed them all, you can tell w

    • Re:

      In practice, I disagree. Whenever I'm writing recursion or a while loop, I always aim for a single-line comment explaining why it terminates, and I ask for similar comments when I'm reviewing code (unless it's trivial, e.g. an integer increment with clear upper bound). I've found quite a few bugs this way in practical systems. And if there's no recursion or while loop, well, it halts!

      Whenever there are two pieces of storage storing related information, I ask for comments explaining the invariants that relat

  • Re:

    This is a misunderstanding of the halting problem. It doesn't say that you can never determine if a program will halt or not, only that you can't determine of all programs halt or not.

    Just because we can't solve the problem all of the time, doesn't mean that we can't solve a problem some of the time, or even most of the time.

    You should be able to easily write a program that you can prove will halt. You can even write programs that will examine other programs and determine if they will halt or not. What

    • Re:

      only that you can't determine of all programs halt or not.
      Nope: only that you can't write an algorithm that proves for every program if it halts or not.

    • Re:

      And to that point, universal computer that only allows halting programs is impossible. You should be able to easily write a program that halts but you cannot have turing-complete language that will allow you to write programs that always halt. Hence, bugs and security problems will still possible in programs written in either C or SPARK or whatever system NVIDIA security team decided to use.
      
      In your hypothetical, if there is a system that can determine if your specific program will halt or not, it will

      • Re:

        That is not necessarilly true.

        I have never used SPARK in particular. But when using code provers, you never just throw you whole code and ask the prover to show it has a property. The properties are expressed from the ground up through the simpler functions to the more complex functions.

        When you realize the prover can't write the proof, you introduce intermediate properties on smaller parts of the code to help it do what you need.

    • • Re:

        It was sloppy and incorrect paraphrasing of the halting problem, most certainly leading to confusion for those that it intended to inform, assuming that was the intention. It wasn't the only slop in the post either.

• They *RECODED* (and that's the key) a C program into SPARK and they want us to believe that the "improvements in the security" (whatever that means because there are no code to check nor testsuites nor nothing) was not because of "recoding" but because of "the language"...

  • Re:

    It is difficult to prove the correctness of C programs because of pointer aliasing [wikipedia.org], out of bounds array accesses, and stack munging [wikipedia.org]. Many other languages don't allow these operations.

    • Re:

      That why all the smart C programmers moved to std::vector and std::string - they can check that for you.

      • Re:

        The problem here is the can. It should be must.

        • Re:

          I believe all the major C++ compilers enable STL range-checking by default these days.

          You can use command line switches to turn it on/off as needed.

          The real problem is convincing C programmers to educate themselves.

          • Re:

            I believe all the major C++ compilers enable STL range-checking by default these days.

            They don't.:(

      • Re:

        Smart C programmers moved to libraries of another language?

    • • Re:

        Let's say you have a million lines of code and one function of 20 lines that modifies and accesses a local array.

        If it is a Rust program, you need to look at 20 lines of code to "prove" the array is consistent (what you write is what you read back).

        In a C program, you need to look at a million lines. Any code can modify any memory location.

        • Re:

          What about a C++ program?

          Anybody trying to write large, "secure" code in C is probably doing it wrong.

          • Re:

            C++ has the same problems as C.

            You can use objects to encapsulate information, but you can also violate that encapsulation by pointing any pointer to any location in memory. So formal verification is difficult.

            • Re:

              C++ will drastically reduce the number of raw pointers in a program (all the way to zero if that's your goal...)

              It also allows iterators, you don't have to constantly pass around the size of things, you also won't be rewriting linked list for the nth time just because you added a new struct.

              It's hard to overstate the gains in safety that are possible in C++ compared to C.

              • This is a religious argument, not an objective one.

                At any time, a C++ programmer can use straight C so your "gains in safety" assume discipline. That discipline can be applied to the C programmer without using C++ at all. It may be more tedious, but you are claiming "possible/not possible". No.

                C programmers are not compelled to use unsafe features just because other languages protect against them.

                I can't remember the last time I introduced a memory leak in a program. Decades. Mostly that's because of the nature of the software I develop, but I NEVER use runtime malloc. I've fixed plenty in other people's code though. While C allows the possibility of memory leaks, it does not compel their existence and it is EASY to "overstate the gains" in this area as it applies to my particular coding style.

                Furthermore, your argument boils down to code hiding. Various unsafe techniques might still be there, but your language supports constructs that destroy visibility into them. This is ultimately the core problem with modern software quality, it's a mile high stack of shit. Right at the center of it, C++.

                As an aside, a long time ago, I worked on a project where performance was paramount. The vendor for our processors sold the company on a promise of 40% performance gains using special software and tools. We denied that it was possible, but I was assigned to pursue the tools with the vendor. After a thorough implementation with the vendor, the speedup was exactly 0%. Why, because the vendor assumed we were incompetent; it turns out everything they were optimizing we had already optimized. Your entire argument assumes the same.

              • Re:

                C++'s safety would be vastly improved if it wasn't saddled with C and older C++ compatibility, but of course, that's also one of it's biggest strengths as a language. The language is largely unsafe by default, with safety features opt-in, and there's no way outside of external tool use (and barely even then), to ensure you're not straying outside the lines. It mostly comes down to sticking to safe conventions and more modern code practices. Yes, you can achieve something fairly close to memory safety the

        • Re:

          If you cannot modify raw memory with Rust, it would mean there are plenty of things you cannot program with that language then.

        • • Re:

            Nope.

            The typical C program passes pointers around everywhere. If it didn't, then everything would have to be passed by value on the stack and new copies of all data made at every function call.

            If you have a function with a dereference of a pointer that has been passed to it, you have to analyze the complete program to find every source of that pointer, and make sure that in each and every case it can never refer to invalid memory at any point during the pointer's lifetime. You don't get to just look at the

  • Re:

    These people are dumbasses. At the end everything ends up as instruction code. It's just not there until it's there.

  • Re:

    I really don't see your point. It's obvious that they didn't just translate the original code into the new language line by line and be done with it. They would have looked at interface boundaries, calling contracts, parameters, inputs, outputs and produced functionally equivalent code using the safe language. Line by line it would look very different.

    It doesn't mean the existing code was safe, or that it would stay safe after being modified. Nor does it even mean you could apply what you learned from the

  • • Re:

      Yep. Sound to me like they just invented a complex way to find bugs in C programs.

    • Re:

      Or... instead of writing in C then fucking around forever playing whac-a-mole on security holes, you could write in a language which is designed to not have a bunch of those problems and gives you a lot of tools for proving correctness relative to a spec.

      Like, gee, imagine if we could use those magical blinkenlight boxes to automate away tedious tasks like auditing the most error prone sections of code for well known bugs.

      • Re: Please, stop treating us as ignorants...

        Like Ada for example.

        • Re:

          That's crazy talk.

          How else am I supposed to prove my awesomeness if I can't claim on the internet to write bug free C code? Really half of the posts on this story read like incredibly dull and exceptionally nerdy letters to penthouse.

        • Re:

          SPARK is based subset [adacore.com] on Ada.

• A company that managed to include a node.js web service with their drivers that exposes privileged system calls to the network, I doubt they would be able to actually use languages with automated proofs.

  • Re:

    Mod Up. The word metrics came up. Normally you then know which coders are best, and write the most trustworthy code, and the others just interested in a paycheck and in the average range. They have enough money to employ some OpenBSD auditors to sample their 'passed' code for more metrics. In the real world this is never done. At university CS, 'Duty Programmers' with nasty red pens are the best. They know how beginners think. These are the people project managers hate, because it is PC incorrect to tell an

  • LOL! ... Really?

    They did that?... I believe you, it's totally thinkable because of the l00ny Node craze and the epic prevalence of dimwitt deciders, but this is a new level of Monty Python in software projects. Pretty hilarious if you ask me. ROTFL!

• I was taught this too. It's a brilliant way of proving your code is bugged perfectly according to specification.
  
  Why? Because at that point the spec is code, and code can be bugged. Also it tells you nothing about implementation - it would tell your your outputs were perfect for all your inputs according to what the specification asked for, but wouldn't tell you you'd forgotten to free a pointer.
  
  My lecturer (we're talking early 90s) was adamant that it wasn't just yet another computer language and was different in concept. It was Z I was taught...and lo and behold, a few years after university, a compiler for it appeared...

  • Re:

    Z might have stood a better chance of succeeding if it was actually readable and writable instead of using mathematical notations that couldn't even be properly encoded or rendered by computers at the time. We had a module on it and we had to write our answers with pen and paper.

    • Re:

      Back then basically all coding assignments where answered on paper with pencil.

  • Re:

    Indeed. Back then, the CS prof teaching us formal verification said he just saw it as a form of an alternate implementation that gets compared to the code. It is not nearly as absolute as most people think and does absolutely nothing (except giving a false sense of security) when the ones writing the spec just make the same mistakes. That is quite common, because a lot of problems result from people missing more complex cases or unexpected behaviors and often they miss them in the code and the spec both, ev

    • • Re:

        Indeed. And you probably are not even talking about a formal spec (which is a lot more precise and a lot harder to do), but a regular spec which is unsuitable for formal verification anyways.

      • Re:

        I usually get specs like, "We need you to add a report to the program that shows various summaries of certain transaction types. Here's the total we got for yesterday. You'll have to figure out what the transaction types are that end up with that number. We'll need to start using it tomorrow morning."

        If I'm really lucky, I'll get a couple weeks notice to fit that in with the twenty five high priority, poorly (if at all) defined issues that needed to be done yesterday.

        Go ahead, SPARK, formally verify that.

  • • Re: Oh lawd, not the formal methods bullshit again

      It becomes quite a lot harder to prove the drawing the route part when its done using nvidia drivers with abritrary performance hacks of the week to win the fps battle for the latest aaa benchmark title...

      Still, you'd think that by now libpng and such that nobody rewrites in latest fashion magic bullet language were proven but apparently not.

• wow! another sucker company that has fallen for provably secure bullshit.

  • Re:

    Yeah. The limits of that approach are well known.

  • Re:

    This is your failure in reasoning, not theirs.

    They are not claiming that using a language that eliminates many classes of bugs solves all problems. It's only you and your fellow C supremacists who arebasically claiming that the only real alternative to C is complete perfection, so therefore it doesn't exist.

    Eliminating certain very common bug classes means you no longer need to spend time auditing for them and fixing them.

    You can write secure machine code given enough time and resources. But it's, frankly,

    • Re:

      I recommend reading "Michael Abrash's Black Book of Graphics Programming". My perspective is that the hardware will do whatever it damn well pleases, regardless of your software. Abstracting away software problems doesn't make the problems go away, it merely hides the problems. Thus C, aka portable assembly, which makes it easier to figure out the difference between what you wrote and what the hardware actually did. Yes, it would be nice to use fancier languages, if only the hardware would play along.

• How is it different CodeSonar static code analysis tool?
  from https://en.wikipedia.org/wiki/... [wikipedia.org]

  https://en.wikipedia.org/wiki/... [wikipedia.org]

  https://en.wikipedia.org/wiki/... [wikipedia.org]

  This seems to be new, but then the specification needs to be correct:

  https://www.adacore.com/about-... [adacore.com]

  DEF CON 30 video links:
  https://blog.adacore.com/when-... [adacore.com]

  • Re:

    Static analysis tools for C/C++ are better than nothing but anyone who has ever used them also knows they are expensive, slow and hopelessly broken, producing reams of false positives or getting easily confused.

  • Re:

    That's kind of ironic because Ada is famous for a certain disaster [bugsnag.com] due to a numerical overflow resulting from a type range violation. `

    • Re:

      Your link has been slashdotted, so here is another https://itsfoss.com/a-floating... [itsfoss.com]

  • Re:

    The best you can do is annotate C(++) and then iteratively modify portions which can not be automatically proven to the point it has Spark level (or higher) correctness guarantees, like the L4 verified project did.

    Ignoring that mountainous level of work, Spark has stronger guarantees than Misra C(++) which has stronger guarantees than free form C(++) with analysis tools.

    • Re:

      The best you can do is annotate C(++) and then iteratively modify portions which can not be automatically proven to the point it has Spark level (or higher) correctness guarantees, like the L4 verified project did.

      Ignoring that mountainous level of work,
      

      Exactly. The ClEvEr PrOgRaMmErS wRiTe BuG fReE C crowd are ignoring that while you can, it usually involves external tools and standards and ton of work. I can never get the reason why they think it's so terrible to have those integrated into the language it

• Had not heard much about that language in years

• For nVidia hardware, simply unplug it and place it in storage.

• It's fun to order a programmer

  To program everything in C
  To patch, install, bug fix and more
  And run at the first sign of bankruptcy!

  It can be manly in programming
  They'll cut your salary semi-annually
  It's not tax deductible
  Our binaries are corruptible
  We're programming in the language known as C

• Yes, testing is limited in what it can do for security. But that primarily applies to logical errors and does apply not or only in a very limited sense to the specific vulnerabilities caused by the absence of memory safety. Hence this is _not_ a reason to give up C and this person has no clue what they are talking about.

  • Re:

    Spark exists and Misra C and its competitors can not provide tool chains able to give equivalent guarantees even if it is theoretically possible. Spark is cheap too.

    By the time you are following Misra type coding guidelines and add range annotation it might as well be a different language any way, that ain't C to me.

• This all sounds very similar to Z and VDM - which at the end of the 1980s early 1990s was clearly going to be the way programming was going. I even put myself on a couple of courses to learn those formal methods - apparently I was guaranteed to get a return on my investment in my upgraded skills (or so I was told). Hohum.

  The problem was, they took time to learn and otherwise perfectly decent programmers couldn't necessarily get their heads around the esoteric nature of formal methods (being based on abst

• C is _a_ problem, but not the core problem. As I explained in my 2005 textbook High-Assurance Design, the core problem is that programmers, by and large, have little-to-no training in secure coding, and even less interest in it. And that is mostly because employers do not make that kind of training a priority. When was the last job interview in which you were asked about your knowledge of secure coding? And that is mostly because companies that write software have insufficient liability for losses when users of that software experience security breaches.

  • Re:

    Back in the days when I was developing a small software demonstrator, we avoided C and C++ as much as possible. Our company did not produce software. It was an experimental project, but it had to run fast. It did some FEM-like simulations on ICs. If it was too slow, it was not worth investigating further.
    I had a fierce discussion about this with one of the programmers. He argued that we had to do everything in C++, because that is the only "real" programming language. It was also going to be a lot faster.

    • Re:

      I agree. Programmers become loyal to the languages they know. That is a dysfunction. Perhaps the reason is that it takes so long to learn a language well. It becomes a constant tool of trade, rather than a tool from the shelf.

  • Re:

    Of course, Python never has any security problems. Neither does Javascript.

    • Re:

      Indeed!! In fact, Javascript is the primary attack vector of most malware!

    • Running on interpreters written in ...

      ... oh, what was it called again..

      oh yeah,

      • Re:

        Oh God if you think the reason there are sql injection vulnerabilities in Python is because it's written in C, then you are a hopeless moron. And that is an insult to morons, I apologize.

  • Re:

    Amongst other things, programmers and software engineers work at:
    1) Functionality (does the software do what it is supposed to, more or less)
    2) Interoperability (using and offering APIs) 3) Maintainability (readable code, documentation, solid yet flexible design and object models, good data models, etc)
    4) Testing (allowing for automatic testing)
    5) Security.
    
    I found that many software developers stop after point 2 or 3. They'll pay lip service to testing ans security, instead trusting that the testing

• What if you just shut the hell up, hmm?

• Replace all old bugs with new bugs. Definitely not against using other languages when possible. Thing is there are only so many was to build low level code.

• Look, this has become a religious war for many.

  The C camp will continue doing C.

  Their competition will use Rust and similar tools.

  We'll see in a few years who's come out on top.

  I would put my money in a bank coded in Rust. Place your bets.

  • Re:

    In a bank? Sure, in a video game? Not so much.

  • Java evangelists said the same thing in the 90s

    Java certainly got traction but nothing like what we were led to believe. Its big in certain sectors for backend dev , eg finance , and for some shitty DB plugins , eg Oracle, but thats about it even thought believe it or not it was originally designed for embedded systems.

• Why SPARK and not Spin [spinroot.com]?

  Spin uses C and not Ada. So it seems like it would be more familiar to NVIDIA's engineering staff. And the step of porting over would be omitted.

  Spin can be used in way beyond what SPARK can offer. From the website:

  Of course if you do an exhaustive verification of a complex program it would take more resources to complete than exist. It's not going to solve the halting problem for you. But for narrow cases you can fully verify and there are examples of real-time schedulers and network

• • Re:

    No it doesn't protect you from errors in application logic. A safe language *does* protect you from the other 50% of bugs which are caused by the lack of safety in C & C++. Things like double frees, buffer under/overruns, null pointer exceptions, data races and so on.

    • Re:

      I agree, but the two concepts are orthogonal. Formal methods does not imply 'safe' language. Safe language does not imply formal methods.

    • • Re:

        At least Half of the CVEs for the Linux kernel are bugs of that nature. Here is a link [cvedetails.com] to them. As I write the results show 1) is a buffer overflow, 2) is a use after free, 4) is a double free, 5) is a lifetime issue, 6) is broken pointer arithmetic, 7) is a use after free, 8) is a use after free. And so on and so on and so on. Chances are other projects, especially closed source ones are far worse.

        But maybe you are Super Programmer, not like those cowboys who work on the Linux kernel and are incapable of

• • Re:

    Read up on the AS/400 architecture, it’s fascinating. Buffer overflows are almost non existent.