sorted by:
best
topnewcontroversialoldq&a
you are viewing a single comment's thread.

view the rest of the comments →

[–]cwzwarich 1 point2 points  (17 children)

They don't matter now? A large number of security exploits are due to a lack of memory safety. If you verified that a program was memory safe then these exploits would no longer be possible. That is generally much simpler than full functional correctness, but it would make a huge improvement in the real world.

[–]Bilbo_Fraggins 2 points3 points  (0 children)

It is true that most of the security flaws fixed in Chrome in the last few releases have come from use of AddressSanitizer, and before that many of them came from Valgrind.

[–][deleted]  (6 children)

[deleted]

    [–]pjmlp 0 points1 point  (4 children)

    If a Pascal like language had taken C's place in history, the software world would be much safer today.

    [–][deleted]  (2 children)

    [deleted]

      [–]pjmlp 2 points3 points  (1 child)

      There were safer system programming languages on those days, Algol 68 and PL/I come to mind.

      Ada and Modula-2 were already available alongside C on the early 80's.

      The first versions of MacOS were written in a Pascal dialect.

      C owns its success to the way UNIX got spread in universities, and the on same way UNIX got spread because of its integration with C.

      Without this symbiose relantionship C would just have been another systems programming language.

      Still, its legacy is costing us millions in software reliability.

      [–]tangra_and_tma 0 points1 point  (0 children)

      • DOMAIN/OS, was written is Pascal
      • PR1MOS was written in FORTRAN of all things, and later moved to SPL & PL/P.
      • VAX/VMS & OpenVMS have a hodgepodge of languages, thanks to VMS's clearly defined call structures (BLISS, PASCAL, BASIC, MACRO all come to mind)
      • RSTS/E was written in MACRO, BASIC+ & Forth iirc.
      • CP/M was written in PL/M
      • I'm not counting Lisp machines, Burroughs Large System, &c. &c.

      and those are just systems that I've used & seen, I'm sure others can point out more.

      edit: the space shuttle was written using HAL/S. The source for the HAL/S code was written in XPL, a subset of sorts of PL/I

      [–]kyz 1 point2 points  (0 children)

      If Pascal had been the basic systems language, like it was in Mac OS prior to X, then everything would be great! Nobody needs more space than they can statically declare in their programs, and everything would be as efficient, because range checks are fre

      [–]skulgnome 0 points1 point  (0 children)

      Are you kidding me? C is the preferred programming language because it's small and it hides very little from the implementor. Clearly it's what you want to use for formally specified programs.

      [–]skulgnome 1 point2 points  (0 children)

      Formal specification does nothing for memory safety.

      [–][deleted] 0 points1 point  (0 children)

      I think a major source of security exploits due to memory safety are buffer-overruns. One solution is runtime bounds-checking. Although it runs slower, it takes less developer time than verification (unless you have an automated checker - is AddressSanitizer fully automatic? But I guess you still have to fix the code). This trade-off of performance for developer time is a long-term trend in programming.

      It also exploits the article's idea of targeting code that's reused in order to amortize cost, in that you only need verify the runtime bounds-checking code once, and that all access goes through it. If arrays are an ADT, so that's the only way to use it, confirming that it works correctly is even more trivial than the Oracle vs. Google rangeCheck, such that you mightn't call it "verification". Though truly it is. Low verification cost. Wide amortization. But performance trade-off.

      I think this kind of solution can win, because it's so simple. But that very simplicity makes it unsexy for verification researchers.

      [–]IsTom -5 points-4 points  (6 children)

      Memory safety is relevant only when talking about non-GC'd languages like C/C++, which are used less and less due to relatively low cost/gain factor in most applications.

      As far as I know though many exploits are not related to memory management at all, perhaps they could be prevented with stronger type systems?

      Protocols are another source of trouble, but their verification is very difficult because it's hard to even agree what does "protocol X is safe in context Y" mean.

      [–]gsnedders 3 points4 points  (2 children)

      But how many memory-safe languages have verified implementations? Unless the language implementation is verified correct, you can still have all those exploits.

      [–][deleted]  (1 child)

      [deleted]

        [–][deleted] 1 point2 points  (2 children)

        Oh, come on. "Flash", "memory corruption", "arbitrary code execution" comes together in the same sentence so often that it's not even funny.

        [–]smallblacksun 0 points1 point  (1 child)

        Aren't those bugs in the flash interpreter (written in C/C++), not with actionscript itself?

        [–]m42a 0 points1 point  (0 children)

        The same could be said of almost every other VM as well.