1. 86
  1.  

  2. 11

    Please someone make openbsd style privsep happen for systemd. It won’t fix all problems but not doing it in 2016 is like riding a motorbike at 200km/h without a helmet.

    1. 11

      Here’s the issue: https://github.com/systemd/systemd/issues/4234 A fix has been commited: https://github.com/systemd/systemd/commit/531ac2b2349da02acc9c382849758e07eb92b020

      That’s a very low-profile answer, no “thanks”, no mitigation info for those who have systemd deployed.

      1. 5

        That’s a very low-profile answer, no “thanks”, no mitigation info for those who have systemd deployed.

        Further reinforcing the message that systemd is a project that simply doesn’t take security seriously.

      2. 14

        Wow that is a bad title.
        1) It has nothing to do with tweets/twitter
        2) It just happens to fit in a single tweet, but length of command has almost nothing to do with the destruction it can cause, see rm -Rf /, fork bombs, tar bombs, cat /dev/random and busy loops, etc.

        1. 19

          Is it so bad? When people were posting “RC4 in a tweet” nobody mistakenly thought you could encrypt something by sending a tweet.

          The amount of text required to describe a problem is one way to measure how easy it is (or should have been) to find. Nobody’s posting “14 stage sandbox escape for chrome in one tweet”.

          1. 6

            I guess, I just interpreted it as “with” rather than “in” one tweet. I think “one line” or “in a one liner” would have been clearer for a quite technical article.

            1. 11

              This is “tweet” as a unit of measurement. 1.4 characters is a centitweet, 100 centitweets makes a tweet, 1000 tweets is a kilotweet and 1000 kilotweets is a twonne.

              1. 2

                It would make more sense if 1.4 chars is a centitweet.

                1. 3

                  Oops, you’re right. I must have messed up the formula while converting from imperial tweets to metric tweets. That’s my story and I’m sticking to it.

            2. 4

              In this case I actually did misinterpret the title to mean something related to Twitter, but that’s just me.

              1. 3

                It is important to specify that it is the length of a Tweet because people have encountered security problems from simply viewing a Tweet or from viewing an SMS that came from a Tweet on Twitter.

                1. 3

                  I do and don’t agree. I agree in that the length input to trigger a bug is often very small. Minimal test cases (such as the author’s empty string) usually expose a lot of edge case behavior.

                  To pilkch’s point, this has nothing to do with Twitter or tweets, just that the command to trigger it is < 160 characters. So long as you take care not to pipe your tweet stream into your shell, you should be safe.

              2. 7

                I also thought it was related to Twitter, but it’s forgivable and what matters is the security issue we are facing at hand, not which title the author chose for his article.

              3. 4

                What choice do we have if we want to run a modern distro, with a healthy package ecosystem, without systemd?

                1. 5

                  Gentoo. Slackware. !Linux. Opinions vary on the “healthiness” of both those distros, but either should be perfectly workable for a desktop system.

                  1. 4

                    The availability of non-systemd init is the primary (perhaps only?) reason I currently run Debian. I’m honestly not hugely enamored of it overall, but being able to run OpenRC (sysvinit is also an option) is a major boon. There have been a few small hiccups here and there with package updates, but for the most part it works quite smoothly.

                    1. 1

                      Do you know what the state of Debian/kFreeBSD is? Infuriatingly it was almost-but-not-quite a first-class-supported thing when systemd came along.

                      1. 3

                        I don’t know the current state (although the mailing list is quite quiet), but it didn’t look great at the time of the 8.0 release:

                        We discussed kfreebsd at length, but are not satisfied that a release with Jessie will be of sufficient quality. We are dropping it as an official release architecture, though we do hope that the porters will be able to make a simultaneous unofficial release.

                        From this mail.

                    2. 1

                      YMMV but I run both VoidLinux and AlpineLinux here for that (and also for musl-libc and in the case of alpine, grsec).

                    3. 7

                      I’m a bit annoyed by all the “good programmers” rhetoric in this post. Show me the “good programmer” that never missed an edge case.

                      Many security bugs are obvious in hindsight.

                      1. 14

                        the issue here is that lessons from history and simply good old programming practices are consciously and judiciously ignored in the development of systemd. that is bad for any software, but especially so for PID 1.

                        1. 3

                          I still don’t buy that (short) argument. Most criticism about systemd is that they don’t follow the unix philosophy (which I disagree with).

                          I don’t see which practices are ignored. Systemd has separation of concerns, relies on declarative configuration over hand-coding and generally works. I think it is a clear win over many other init systems.

                          Sure, the bug is embarrassing, but the post still doesn’t make a good case for why it is bad software in general. Other then the author believing that they are a better programmer.

                          1. 11

                            I don’t see which practices are ignored.

                            Read it again. Pay particular attention to the umask(0); example.

                            As you say, even the best programmers make mistakes. But systemd by design amplifies those mistakes through fail-open decision making and a stunning lack of privilege separation, both of which fly in the face of completely standard security practices.

                            It chooses to create files as vulnerable by default and assumes that programmers will perfectly and always lock down sensitive files, when the reverse would be standard practice. It chooses to parse messages in PID 1, instead of in a least-privleged helper process, leading to the very bug this thread is about. Again, the reverse would be standard practice.

                            1. 10

                              Previous arguments that systemd did too much as pid 1 were countered by saying that it didn’t, and it actually uses many processes. This seems like a counter counter example that too much user input is being handled.

                              1. 7

                                Then let me share with you the best counterpoint I ever saw which I received after similarly mocking one that seemed just too tiny. I even changed my opinion quite a bit as it gave me plenty clarity. It’s this simple:

                                1. PID 1 failures can screw up or take down your whole system. Ultra-critical issue.

                                2. Keeping PID 1 tiny and correct with risky shit outside of it, preferably enforced by MMU, with mediated interactions prevents such whole-system failures vast majority of the time. Like such techniques do with most other components.

                                BOOM! That simple. It’s also a principle from high-assurance that was field-proven going back decades in fielded systems leveraging the TCB concept. Whatever you trust the most must be simple enough to evaluate with best tools, code review, etc. Preferably, proven correct-by-construction in specific ways (see CompCert or seL4) or free of specific problems (see Astree Analyzer or SPARK). Another heuristic was that you should be able to express it concisely… leaning toward hundreds rather than tens of thousands of lines… in an abstract, precise spec that covers all successful and failure states. If you can’t, it’s probably too damned complicated to make error free in C code or whatever. Upper limit at one point for full, formal verification of abstract implementation (not concrete code!) was 10,000 lines of code. seL4 established new limit by doing it for code. So… still 10,000 lines for highest confidence but now in code itself. Let’s apply these heuristics. This thread which was first I could find for comparison…

                                https://www.reddit.com/r/linux/comments/2hkx5v/clearing_up_a_little_bit_of_misinformation_about/

                                …aims to clear up misinformation about SystemD’s large size by saying it only has 94,000 lines of code or maybe as little as 63,000 depending on how you count. The one below has 87 lines in the main function with Reddit link saying two dependencies might be around 9,000 lines.

                                http://git.suckless.org/sinit/tree/sinit.c

                                They could’ve mathematically modeled, proven, and exhaustively tested that little sucker (err suckless alternative) using the shitty tools they had in the 1980’s on equally-shitty machines. The same computers and tools would’ve crashed trying to simply model-check a non-trivial property of the entirety of SystemD code. I think they couldn’t even load the full source on the microcomputers like Apple II until it was enhanced several times. Then no room left for apps! We can’t get to other heuristics since it already failed at max size for low bugs vs competition. Old principles of KISS design & implementation of TCB means the lightweight components for PID 1 are objectively better if its reliability or security is high-priority. That as a priority is somewhere way on the bottom for people in some camps, though. ;)

                                Note: Actually, Microsoft claimed to have used VCC to check 20% of their Hyper-V’s 100,000 lines of code against its formal specs after merely several years by full-time, bright researchers with cutting-edge tooling. That’s 20,000loc vs 63,000-94,000loc in SystemD. We might see tooling in our lifetime that can tell us SystemD works correctly. Meanwhile, trusting it is an act of faith instead of reason given historical evidence of what happens to complicated code in critical places.

                            2. 6

                              You are right, we are still humans after all. However, we can limit the risk by designing simple software. The heuristic is that there usually is one critical bug in 1000 LOC, no matter how good you are. So when there are two projects with the same number of people maintaining them, one being 1000 LOC and the other being 10000 LOC while they are doing the same job, I would go for the former.

                              Now you might say: For sure there must be something “useful” in those 9000 LOC. The goal though is to design software that does one thing and does it well, avoiding featuritis and bloat. Apart from security concerns, I think we all have to ask ourselves if the monolith that systemd is is really the direction we should be heading and if we can do it better. And more importantly, if we even have the chance to come up with something better and more secure in a few years when everybody has embraced systemd userspace libraries. It’s the same thing as we had with Pulseaudio, GNU coreutils and bash. All these GNUisms and special libraries are really hindering progress here. It shouldn’t matter which init system, set of core utilities or shell you are running, as long as they all align to Posix or some other ruleset everybody agreed on. Monoculture is harmful. We have a set of standards and many GNUism flags are just plain insane and there is no reason for them to be there (cat -v, echo -e and others for instance), given other utilities do this job.

                              1. 5

                                I don’t think LoC is the first heuristic you should reach for when assessing security risk. If the 1000 LoC project was written in C and the 10000 LoC project was written in a memory safe language I would pick the latter every time. Likewise, if there was a 100000 LoC project written in Coq that came with a proof of correctness, I’d prefer that.

                                1. 5

                                  In the scope of TLS libraries, init systems and core utilities, they are almost all written in “memory unsafe” languages, mostly C. I don’t like the term “memory unsafe”, because good data structures in C can prove to be very effective in reasoning about memory management. It’s just that with OpenSSL for instance, they went way too far and overdesigned everything (BIO_free and consorts) and we see with LibreSSL how it should go. It’s easy to demonise C or other languages with manual memory management, but they will stay with us given the huge drawbacks of languages that try to do memory management for you. I only use C and Go for my projects and it works out. It’s really easy to just say “well, C sucks, because it’s memory unsafe”, but like any tool, you have to use it right. If you know your tool, and know how to use it, there’s no problem with C whatsoever. There are just tasks that are better solved in memory managed languages, especially when you do complex parsing and other things with a lot of string fiddling. But even there, you might end up writing code that is very inefficient, reallocating lots of stuff in the background. With C, you get to feel this complexity and can think of simpler ways to approach a problem. Knowledge of memory “unsafe” languages is in my opinion the foundation for writing good memory managed language code.

                                  Now the LOC heuristic: As the term says, it’s a heuristic. I bet one can write a TLS library in APL with 20 LOC, but that’s unrealistic. Same with proofs of correctness, they are rare as hell, especially in contexts with huge side-effects. In the context of TLS libraries, init systems and the like, where most code is close to the hardware and written in C, you can easily compare with this heuristic, and it served me well in the last few years.

                                  If you allow me to give an example, we implemented Posix core utilities in our project called “sbase”. Now, just compare the implementation for yes(1) in both GNU coreutils and sbase and you’ll see what I mean. Keep in mind, both do exactly the same thing: sbase yes.c, coreutils yes.c. Feel free to browse other examples.

                                  One can give even better examples with musl vs glibc. And keep in mind: All memory safe languages build on top of memory unsafe languages and libraries like glibc and musl, so it is also in your best interest that these pieces of code are secure and not bloated.

                                  1. 7

                                    I don’t like the term “memory unsafe”, because good data structures in C can prove to be very effective in reasoning about memory management.

                                    Just because you don’t like it doesn’t mean it’s untrue. And saying C is “memory safe” when you “just use it right” is silly, because a fair majority of the time people aren’t using it in what you consider the right way to be.

                                    Also, I think there’s a misunderstanding here, where you imply “safe memory management” means “no manual memory management”. It’s been proven that type annotations can be used to check the correctness of manual memory management, such that a manually memory managed language can be considered memory safe.

                                    1. 3

                                      I’ll add you can do it even at the hardware level for C programs if toolchain is modified to give it memory-safety. It’s called Watchdog:

                                      http://www.cs.rutgers.edu/~santosh.nagarakatte/papers/isca12_watchdog.pdf

                                      So, safe and manual management of memory can be done at formal, compiler, and hardware levels these days without a GC.

                                    2. 6

                                      In the scope of TLS libraries, init systems and core utilities, they are almost all written in “memory unsafe” languages, mostly C.

                                      There’s an OCaml library for TLS now. As for init or core utils I see no reason at all such things would need to be written in C (and indeed a quick search turned up e.g. https://github.com/rxse/lyrica ).

                                      It’s really easy to just say “well, C sucks, because it’s memory unsafe”, but like any tool, you have to use it right. If you know your tool, and know how to use it, there’s no problem with C whatsoever.

                                      The truly facile thing is to say “it’s just a tool and if you’re a good programmer there’s no problem”. There really are good and bad tools, and the ability to judge one from the other is what makes a good programmer, far more than outright talent does.

                                      sbase yes.c

                                      Is that supposed to be an example of readable/maintainable code? Because it doesn’t look so to me.

                                      All memory safe languages build on top of memory unsafe languages and libraries like glibc and musl

                                      This is not a law of nature. I have a friend who’s writing rust tools that make system calls directly, without needing libc; unikernel approaches in OCaml are gaining some traction. Not all the pieces are there yet, but a future where we run unikernels or non-libc binaries on a provably secure hypervisor or microkernel (e.g. seL4) seems distinctly plausible.

                                      1. 2

                                        apologies for an off-topic question: I consider myself a “well plugged in” observer of the unikernel “scene” as it were and I’ve come across nothing regarding the use of a secure hypervisor and/or seL4 with unikernels. do you have anything you could point me to? I am insanely curious about this intersection of technologies.

                                        1. 2

                                          They’re mostly commercial. Green Hills did their first desktops on their RTOS w/ Intel vPro in around 2005. Current version is branded “Dell Secure Consolidated Solution.” Genera Dynamics partnered with NSA, VMware, and Red Hat for inaccurately-named HAP workstation. LynxSecure and VxWorks MILS followed with all doing desktops, laptops, servers, and thin clients. Sirrix TrustedDesktop is built on Turaya, which started as Perseus project below. It has microkernel, TPM, VPN, and disk crypto that they polished and built on. One of academic competitors spun off into GenodeOS project that integrates many best-of-breed components with UNIX stuff to try to get a desktop together. Much of the work went into phones or embedded systems, though, because mainstream OS’s cost a lot to redo clean ($200+ million for Solaris 10) while there’s almost no financial demand for secure systems. Last attempt that combined some high-security features with low-assurance components just to keep features and speed high with cost low were Compartmented Mode Workstations. Market killed all of them with Argus probably last supplier still selling well on poor, but popular, foundations. They have a nice summary of things they changed in UNIXen to counter various issues.

                                          http://www.ghs.com/news/20050419_secure_products.html

                                          https://gdmissionsystems.com/cyber/products/trusted-computing-cross-domain/trusted-multilevel-computing-solution/

                                          http://www.perseus-os.org/content/pages/Overview.htm

                                          https://genode.org/

                                          https://www.defcon.org/html/TEXT/8/db-8-Mythrander.ppt

                                          1. 1

                                            Afraid not; that’s what I meant by “not all of the pieces are there yet”. It seems like a natural fit, but I’ve not seen anyone do it yet.

                                          2. 0

                                            There’s an OCaml library for TLS now. As for init or core utils I see no reason at all such things would need to be written in C (and indeed a quick search turned up e.g. https://github.com/rxse/lyrica ).

                                            It’s the other way around: There’s no reason for these things to be written in any high level language. Look at LibreSSL again, it proves a point. It’s not the language that is the issue, it’s the people that introduce cruft. Or check out sinit. You don’t need OCaml shoved on top of it.

                                            The truly facile thing is to say “it’s just a tool and if you’re a good programmer there’s no problem”. There really are good and bad tools, and the ability to judge one from the other is what makes a good programmer, far more than outright talent does.

                                            What you intend to say is “use the right tool for the job”, and that’s exactly what I said above. I use Go for fucks sake, because C sucks for many things and Go can really make your life easier.

                                            Is that supposed to be an example of readable/maintainable code? Because it doesn’t look so to me.

                                            If you flex your brains a bit you’ll easily understand what it is about. Each line has a certain weight, and the main loop might take a bit to understand, but it’s not rocket science. It’s way different from the coreutils one, because there, before you even get to study the main loop, you have to think about the side-effects of initializemain(), setprogramname (), bindtextdomain(), textdomain() and figure out how parselong_options() works. I bet this takes much longer than figuring out how the one main loop in the sbase yes.c works. And if you are so inclined, you can feel free to split the loop up into two, nobody stops you from that. The thing with maintainable code is that some snippets of code don’t even need maintenance. They just work.

                                            This is not a law of nature. I have a friend who’s writing rust tools that make system calls directly, without needing libc; unikernel approaches in OCaml are gaining some traction. Not all the pieces are there yet, but a future where we run unikernels or non-libc binaries on a provably secure hypervisor or microkernel (e.g. seL4) seems distinctly plausible.

                                            Of course you can do that, but 99.9% of high level languages use C standard libraries and I don’t care about people who put together some rusty (get it?) stuff alone in their barn.

                                            1. 7

                                              Look at LibreSSL again, it proves a point. It’s not the language that is the issue

                                              LibreSSL still frequently suffers from vulnerabilities. The language is the issue.

                                              it’s the people that introduce cruft

                                              Good luck improving people. Much easier to make languages that work even when people use them.

                                              Or check out sinit. You don’t need OCaml shoved on top of it.

                                              “for (i = 0; i < LEN(sigmap); i++)” is more than enough reason to switch that to a better language.

                                              What you intend to say is “use the right tool for the job”

                                              That’s utterly useless as a heuristic for actually making decisions. “never use C, always use OCaml” is much better advice, because when applied by an ordinary developer it leads to making a better decision most of the time than “use the right tool for the job” does.

                                              Of course you can do that, but 99.9% of high level languages use C standard libraries and I don’t care about people who put together some rusty (get it?) stuff alone in their barn.

                                              99.9% of people use glibc and don’t care about musl. 99.9% of people use coreutils and don’t care about sbase. So that seems a rather self-defeating attitude.

                                              1. -7

                                                “for (i = 0; i < LEN(sigmap); i++)” is more than enough reason to switch that to a better language.

                                                Sorry man, but this just proves your incompetence. Keep using your “smart iterators” and “type inference” while I keep writing real and secure code in C.

                                              2. 4

                                                The thing with maintainable code is that some snippets of code don’t even need maintenance. They just work.

                                                How will anybody be able to review your code to help catch security vulnerabilities if it takes several hours of meditation to read your implementation of yes.c?

                                                1. 3

                                                  I didn’t understand this post until I actually clicked the link. It is overly clever, as if its primary goal was to be “poetic” rather than “useful.” It is the exact kind of thing I would flag for further consideration in a code review. Was this picked to prove my point that LoC isn’t a great heuristic?

                                                  1. 2

                                                    That’s just the Suckless way, aka Write everything like we’re doing code golf so our SLOC is smaller

                                                  2. 1

                                                    Yeah, that’s going too far. The size, structure, and language must work together for best comprehension. That’s for humans and verification tools.

                                                    1. -6

                                                      Well maybe that proves a point. If you are not qualified enough to understand this simple loop you might as well just quit software programming. Some tasks are just too difficult for the common folk.

                                                      1. 7

                                                        “not qualified” “quit software programming” “too difficult for the common folk” and elsewhere “this just proves your incompetence”

                                                        You are embarrassing yourself.

                                                        1. 3

                                                          Was I implying that junior engineers would be doing your code reviews? That’s hilarious. It doesn’t matter how senior or wise of a programmer you are, there’s code that’s easier to review and code that’s meaninglessly difficult to review. Doesn’t make it impossible, but it sure makes for a waste of time, and it quickly builds the barrier to reviewing complete suites of real-world software and understanding bugs that involve the interaction of smaller pieces of code like that.

                                                      2. 4

                                                        “It’s the other way around: There’s no reason for these things to be written in any high level language. Look at LibreSSL again, it proves a point. It’s not the language that is the issue, it’s the people that introduce cruft.”

                                                        That’s incorrect. One should use best tool for the job. The best tool, if there was an objective definition, is probably the one that achieves the programmers' goals as quickly, correctly, and low-maintenance as possible. The Ocaml implementation has acceptable performance for most users. The code is more concise, much of it pure (easy analysis or proofs), and the rest immune by design to specific errors. A different implementation by INRIA and Microsoft in F star was mathematically verified against the spec on top of a lot of testing. That means, if the abstract spec and tiny proof-checker are correct, then the system will behave according to success or error specs in all input situations.

                                                        LibreSSL, much as I’ve praised their effort, comes nowhere near close to the level of assurance Ocaml people get against code injection and is 20 ballparks away from verified one in arguing its correctness. Their own comments in the commit log indicated that despite them being excellent C coders. That the Ocaml project succeeded to do so much of TLS clean-slate with those attributes and immunity to key errors with a small team in a few years says plenty about the quality of language and tooling. Smart C developers work much harder to write less software that comes with more qualifiers about safety/security. It does run app’s code, malicious code, or error code some percentage faster, though. ;)

                                                    2. 2

                                                      yes.c

                                                      So… why exactly is that loop written like this:

                                                      for (p = argv; ; p = (*p && *(p + 1)) ? p + 1 : argv) {
                                                          fputs(*p ? *p : "y", stdout);
                                                          putchar((!*p || !*(p + 1)) ? '\n' : ' ');
                                                      }
                                                      

                                                      … instead of like this?

                                                      for (p = argv; ; *p || (p = argv)) {
                                                          fputs(*p ? *p++ : "y", stdout);
                                                          putchar(*p ? ' ' : '\n');
                                                      }
                                                      

                                                      Is it supposed to be incomprehensible? (Or inefficient?)

                                                      1. 2

                                                        All memory safe languages build on top of memory unsafe languages and libraries like glibc and musl, so it is also in your best interest that these pieces of code are secure and not bloated.

                                                        Your comments about this mostly sound good. I referenced the suckless init in mine. I have to point out this one is a myth that comes with fact that most languages bootstrap on or deploy using C or C-based components like those mainly for convenience of not rewriting everything (esp compiler optimizations or OS’s). Also, easy deployment. Oberon OS’s didn’t need it and were simpler. LISP machines didn’t need it. PreScheme was more powerful but also native. SPARK Ada, if your program is static, has no GC but is provably immune to the most common errors. Clay, Cyclone, and Rust can do dynamic safety at compile time. Concurrent Pascal, Eiffel SCOOP, and Rust can do concurrency safety at compile time. Ada & Eiffel can catch many integration errors compile-time. Modula-3 was modified with type-safe linking, too. Haskell, used in House OS, can do even more. A few of these that each have pieces of safety puzzle are actively developed with A2 Bluebottle OS in Oberon being usable and fast. Lacks popular applications due to again… need to rewrite everything going back decades for it and lack of Oberon coders that appreciate such a task. ;)

                                                        You don’t need musl, glibc, or even C to write memory-safe programs or even the underbelly of a memory-safe language. That’s a myth. It’s convenient but not necessary. Musl could’ve itself been done in SPARK with C interface or something like that like Martes or Muen kernels do. Now possibly Rust given they’re implementing GC’s and OS’s like Redox in it. TALC team, Microsoft Research, and Myreen et al even have ways to do assembly with memory-safety verification. Memory unsafe crap is just most system programmers' and users' preference for largely social or economic reasons as good as compiler, analysis, and verification tech is today.

                                                      2. 2

                                                        “I don’t think LoC is the first heuristic you should reach for when assessing security risk. If the 1000 LoC project was written in C and the 10000 LoC project was written in a memory safe language I would pick the latter every time.”

                                                        Yeah, but these kernel/OS programs are almost always written in C. So the counter is meaningless. It’s a well-established principle, from high-assurance security all the way to DJB, that what a program will do across a wide range of input and environmental context will, as code is added, go from decidable to kind of analyzable to difficult to impossible so lets hope some tests catch it. It’s why “reduce code” and “reduce trusted code” were in DJB’s lessons learned from Qmail paper. These principles consistently help. Likewise, OpenBSD partly avoids piles of 0-days by avoiding piles of bloat they don’t need. So, it’s a nice heuristic even if it’s not the last answer.

                                                        “Likewise, if there was a 100000 LoC project written in Coq that came with a proof of correctness, I’d prefer that.”

                                                        I wouldn’t by default. I’d carefully assess the assessments by pro’s of that project. Read my comment to see why:

                                                        https://lobste.rs/s/ml9sb1/how_crash_systemd_one_tweet/comments/gu9oqa#c_gu9oqa

                                                        1. 1

                                                          Yeah, but these kernel/OS programs are almost always written in C. So the counter is meaningless.

                                                          I am merely responding to “however, we can limit the risk by designing simple software” followed by discussion of LoC, as if that was the most relevant concern when designing secure software. I’m aware much of this software is written in C (which I happen to think is a bad idea) but that isn’t germane to my point.

                                                          I wouldn’t by default. I’d carefully assess the assessments by pro’s of that project. Read my comment to see why:

                                                          I don’t see what in that post is relevant to my assertion about Coq, but it was long so I may have missed something. Can you please restate? I will note that 1) a 100k Coq program does not imply a long spec, merely a long proof (which you don’t have to read, the computer will handle it) and 2) the only part of that code that needs to go in your TCB is the Coq type checker, which is small.

                                                          1. 1

                                                            Re simple software & loc. It’s not the only consideration but it’s important if it reflects intrinsic complexity of program’s behavior.

                                                            Re Coq. Well, that’s different. I was countering specs. Anyone that told me they did a 100Kloc program verified fully in Coq is probably full of shit. A manageable spec that produces 100Kloc of machine-checked proof is totally different. Still worth vetting in case directed poorly but TCB is smaller as you stated.

                                                            Re TCB is checker. I about spit my drink out. You wish it was that easy. Your TCB using Coq is all hardware it runs on, any hardware with DMA access, its OS, anything implementation language depended on, the proof checking core, the spec itself, and any critcal stuff like I/O or interruptions outside of it. There’s a reason high-assurance field has worked on verified stacks from CLI’s on FM9001 to Verisofts on VAMP to Myreen et al’s which even makes provers and extraction mostly untrusted. All that used ACL2, PVS, and HOL. Coq is ahead on usability but behind on making TCB as untrusted that Im aware of. But, yeah, your TCB in Coq programs is huge like most formal tools. It helped get funding to whole-stack verification.

                                                            1. 1

                                                              Well, blame yourself for your drink, as that isn’t what I meant at all. I did not mean that the TCB is Coq, but rather that if you want to trust a Coq program implements its specification, the only addition to your TCB is the Coq type checker. The only reason I bring up a TCB is because I saw it in your post and was making a guess that that is the part you considered relevant to the discussion.

                                                              1. 1

                                                                Nah, blame isn’t totally on me this time. Your first statement was a 100Kloc Coq program that “came with a proof of correctness.” Implying it was extra. Most Coq professionals intentionally mean it’s 100Kloc in specs when they say a 100Kloc Coq program since the proofs are always mentioned separately. I rarely see a counterexample on that. Now, you say you brought up TCB since I mentioned it but your usage makes me wonder if anyone told you what it means. A TCB is everything you trust for your claim to be correct. In case of Coq, you’re trusting the underlying OS plus specs as you’re doomed if they’re wrong plus type checker design & implementation plus the logic or extensions themselves. You might also be trusting the tactic system not to give BS directions to the proof effort but the pro’s don’t seem to worry about that. At some point, you have to convert that to code or pull it out of handwritten code. You are also trusting the generation or extraction mechanism. Then, you have to trust whatever makes that machine code and links it into things. And you have to trust whatever process, from logics to specs to code to hardware, led to building all that. :)

                                                                So, your TCB when you use Coq vs just writing a C program or whatnot is much, much larger than you think. Many formal logics, programs, and steps that must work in order for what you wrote to be correct in specification and execution as machine code. Many smart people behind Coq and HOL are trying to eliminate above steps from TCB with clever work but most projects do not. They either assume it’s correct because it used Coq etc or they state the assumptions while hoping they’re correct. That the elite of formal verification are working to eliminate them from TCB just corroborates they’re already in it as I said. It’s not just a proof checker you trust over regular OS. Also, I predict a certifying compiler is even more necessary with the extracted ML programs as there’s been much less research into securing low-level versions of those than imperative programs. Probably attacks waiting to be discovered as more interest grows.

                                                                1. 1

                                                                  Now, you say you brought up TCB since I mentioned it but your usage makes me wonder if anyone told you what it means.

                                                                  I’m sorry that we seem to have a failure to communicate here. I asked up front for you to restate the portion of your post that you felt was relevant to the discussion, and provided two clarifications to my position that I hoped would serve as groundwork for a productive technical discussion. Instead of doing that you are nitpicking about something completely tangential and being particularly condescending about it. Have a good one, and guard your drink carefully while reading lobste.rs–wouldn’t want you to lose it the next time you read a Totally Stupid Post™.

                                                  3. 3

                                                    Doesn’t work on my system. Has anyone had success?

                                                    1. 6

                                                      I though that it hadn’t work on my ubuntu system until I tried to reboot.

                                                      It then failed to shutdown cleanly. This was on:

                                                      fred@MB-A218-01-LAPX:~$ uname -a Linux MB-A218-01-LAPX 4.4.0-38-generic #57-Ubuntu SMP Tue Sep 6 15:42:33 UTC 2016 x86_64 x86_64 x86_64 GNU/Linux

                                                      fred@MB-A218-01-LAPX:~$ lsb_release -a

                                                      No LSB modules are available.

                                                      Distributor ID: Ubuntu

                                                      Description: Ubuntu 16.04.1 LTS

                                                      Release: 16.04

                                                      Codename: xenial

                                                      1. 4

                                                        Good spot. Same for me with Debian 8.

                                                      1. 3

                                                        From the article:

                                                        In particular, any code that accepts messages from untrustworthy sources like systemd-notify should run in a dedicated process as an unprivileged user. The unprivileged process parses and validates messages before passing them along to the privileged process. This is called privilege separation and has been a best practice in security-aware software for over a decade.

                                                        Technically, it’s called input sanitization: making sure untrusted input is sane prior to acting on said input. Also, the trusted process should do the same input sanitization as the untrusted process. All validation/sanitization should be repeated across boundaries when possible.

                                                        1. 3

                                                          Technically, running in an unprivileged process is the privilege separation part. The parsing and validating message is the sanitization part. You can do sanitization in pid 1 if you want to I suppose but then bugs in your sanitization code can compromise pid 1. And since sanitization works with some of the most dangerous data your code will encounter doing it in pid 1 seems like a bad idea. Thus the longstanding best practice of privilege separation.

                                                        2. 2

                                                          :(){ :|:& };: <– will fill up the process counter on any unix machine and make it non responsive. From inside docker it will freeze the host system too docker run busybox “:(){ :|:& };:”

                                                          1. 6

                                                            Forkbombs are trivially mitigated by user process limits. And in any case, the severity of the problem is not the issue (it’s at worst a partial DoS from local code execution, a position from which you can do much more interesting, dangerous things); it’s the reflection of the attitude of the SystemD developers that “eh, I’m sure I know what I’m doing” despite all evidence to the contrary that’s concerning.

                                                          2. 1

                                                            Someone who replied to this on Twitter got “Connection refused”, so this crash won’t work on all systems.

                                                            1. 2

                                                              There is one line on the post stating: “Some people can only reproduce if they wrap the command in a while true loop. Yay non-determinism!”

                                                              I did not try it yet.

                                                            2. 1

                                                              I don’t understand how we are as an industry so incapable of critique without name calling.

                                                              The systemd developers understand none of this, opting to cram an enormous amount of unnecessary complexity into PID 1, which runs as root and is written in a memory-unsafe language. The truth of this statement is irrelevant. Why couldn’t this have been written in a way that criticizes the design rather than the authors?