1. 5

    Product placement and press release. :(

    1. 4

      This is significant news in an important sector of our industry. Your reflexive negativity is destructive to this website.

      1. 8

        I don’t think the personal attack was necessary here.

        1. 11

          This is significant news in an important sector of our industry.

          Sure, but unfortunately we have somewhat limited space and attention bandwidth here, and if we were to support posting every piece of significant news in important sectors of our industry, we’d find ourselves flooded. There is a great site with news for hackers–this sort of stuff is a great fit for that other site!

          Your reflexive negativity is destructive to this website.

          I’m sorry if that’s how this is perceived. I’ve gone to some lengths to do better in terms of negativity. Unfortunately, it’s hard to be positive when pointing out pathological community behaviors that have actively ruined and destroyed other sites.

          1. 2

            I think you’re somewhat right– I would have posted a more technical take like this one but didn’t see any posts about it at the time. After the other one was posted, I would have deleted this one if I was able to.

      1. 1

        defer() is basically independent of the rest of the library, isn’t it? Might want to extract that.

        1. 2

          It’s not entirely independent, as it depends on the "it" macro to create a bunch of variables and run the deferred statements. A stand-alone implementation would require a macro you call at the beginning of a block which will contain deferred expressions, and a macro you call before every return, so it’s not as nice to use. It also relies on GNU extensions, which imo is okay for a test suite, but I’d be careful relying on them in regular code.

          Anyways, I did the work to extract it into its own small library: https://gist.github.com/mortie/0696f1cf717d192a33b7d842144dcf4a

          Example usage:

          #include "defer.h"
          #include <stdio.h>
          int main() {
              defer_init();
              defer(printf("world\n"));
              defer(printf("hello "));
              defer_return(0);
          }
          

          If you want to do anything interesting with it, feel free to.

        1. 3

          I’m still looking for a test harness that doesn’t need me to explicitly call each test/suite in main. My current approach is a simple-minded code-generation. Is there a way to do this that avoids autogenerating files and whatnot?

          1. 3

            There’s a couple of ways I can imagine that would be possible. Currently, each top-level describe generates a function; I could have a global array of function pointers, and use the __COUNTER__ macro to automatically insert describe‘s functions into that array. However, that would mean that the length of the array would have to be static. It probably wouldn’t be too bad though if it was configurable by defining a macro before including the library, and defaulting the length to something like 1024, though.

            Another solution would be to not have these top-level describes, and instead have a macro called testsuite or something, which generates a main function. This would mean that, if your test suite is in multiple files, you’d have to be very careful what you have in those files, because they would be included from a function body, but it would be doable.

            I think the first approach would be the best. You could then also have a runtests() macro which loops from 0 through __COUNTER__ - 2 and runs all the tests.

            1. 1

              That’s a great idea. Thanks!

              1. 2

                An update: the first solution will be much harder than I expected, because you can’t in C do things like foo[0] = bar outside of a function. That means you can’t assign the function pointer to the array in the describe macro. If you could append to a macro frow within a macro, you could have a macro which describe appends to which, when invoked, just calls all the functions created by describe, but there doesn’t seem to be any way to append to a macro from within a macro (though we can get close; using push_macro and pop_macro in _Pragma, it would be possible to append to a macro, but not from within another macro).

                It would still be possible to call the functions something deterministic (say test_##__COUNTER__), and then, in the main function, use dlopen on argv[0], and then loop from i=0 to i=__COUNTER__-2 and use dlsym to find the symbol named "_test_$i" and call it… but that’s not something I want to do in Snow, because that sounds a little too crazy :P

                1. 1

                  I appreciate the update. Yes, that would be too crazy for my taste as well. (As is your second idea above.)

                  1. 1

                    FWIW, you can do this by placing the function pointer in a custom linker section with linker-inserted begin/end symbols; unfortunately, that requires your user to use a custom linker script, which will be annoying for them.

            1. 14

              All of my upward moves have been internal, and of the form “well, we agree that I’ve been doing the job pretty successfully; let us make my title match what I’m actually doing”. IME, seniority is as much taken as it is given. (Not sure to what extent my experience is typical.)

              (E.g. if you want to lead, mentor an intern/junior/…, or arrange to lead a small low-stakes internal project; if you want to architect, shadow an experienced architect, provide designs for your own components, and/or propose important refactorings; etc.)

              1. 7

                IME, seniority is as much taken as it is given.

                Bingo. Show initiative in a polite yet assertive way, deliver results, and talk about those results to the right people.

                1. 4

                  seniority is as much taken as it is given

                  This sounds like good advice. Perhaps it is more applicable to intra-company movements than moving to a new company. Hiring markets are probably be more efficient than intra-company hierarchies; that is, internally companies could be stifling a lot of value by not helping juniors move into seniority, and this inefficiency can be capitalized on by just taking the responsibilities of seniority for yourself.

                  1. 3

                    IME moving between companies is always where you move up

                1. 5

                  Several people here are recommending CMake as an alternative. I’ve only interacted with CMake at a fairly surface level, but found it pretty unwieldy and overcomplicated (failed the “simple things should be simple” test). Does it have merits that I wasn’t seeing?

                  1. 3

                    CMake can generate output both for Unix and for Windows systems. That’s one (good) reason lots of C++ libraries use CMake.

                    1. 2

                      CMake is pretty nice and has nice documentation. You can also pick stuff up from reading other people’s CMakeLists. For simple projects the CMake file can be pretty compact.

                      1. 3

                        I actually found the CMake documentation to be quite terrible for new users. The up-to-date documentation factually describes what the different functions do, but has very little examples of how to actually write real-world CMake scripts. There are a few official tutorials that try to do this, but they are made for ancient versions like CMake 2.6. So in order to learn how to use CMake, you are stuck reading through tons of other peoples scripts to try to deduce some common best practices.

                        While modern CMake is not terrible, you often have to restrict yourself to some ancient version (2.8.6 I believe is common) in order to support certain versions of CentOS/RHEL/Ubuntu LTS (and there were some big changes in CMake around 2.8.12/3.0).

                        Also, having string as the only data type has led to some absurd corner cases.

                      1. 4

                        While small on the surface, it can’t stand alone — it includes bsd.prog.mk has some, ahem, complexity.

                        (I couldn’t tell if your comment implies BSD makefiles are hairballs or if it implies they’re simple ;))

                        1. 3

                          bsd.prog.mk is quite the library, but CMake is much larger; I think it was meant positively.

                      1. 37

                        It wasn’t hate speech directed at some group. It was a self-described “hate post” with a one-line knee-jerk brush-off of Electrum. That’s a worthless troll.

                        I only meant to delete the parent comment and didn’t expect the entire thread to get deleted. I’ll see if I can restore the thread without it, but moderation options are pretty limited.

                        In hindsight, I see how the moderation log was misleading if you didn’t recognize the comment and will write more useful messages.

                        1. 6

                          Yeah, this seems to be a bug, probably because it’s a top-level comment.

                          1. 4

                            It’s not a bug but no reason was given. Not sure if I should reverse that or not.

                            1. 1

                              I did reverse it.

                            2. 3

                              Woo, glad it’s not a new mod policy :D - Thanks for digging in!

                            3. 6

                              I’m not sure if you made the right call here, but thanks for your efforts - communities need moderation, and it’s a hard and often thankless job. I’m happy that lobste.rs does have people willing to take that job!

                            1. 1

                              This is quite neat. One question from someone who didn’t compile the code and play with it: the “XML diff” algorithm BULD seems almost insensitive to ordering, but the order of text matters a lot (and classic diff - and your merge algorithm - are very linear comparisons.) Does the algorithm “behave” once you start moving blocks?

                              Thanks for sharing!

                              1. 2

                                BULD works on ordered trees—that was one of the reasons it was chosen. And it indeed supports the “move” concept in the edit script. In the lowdown implementation (specifically, in the merging algorithm), moves are made into insert/delete simply for the sake of readability of the output. It’s straightforward to extend the API to have “moved from” and “moved to” bits. Then have a little link in the output. Maybe in later versions…

                              1. 1

                                (Minor typo: “rooted at thd node”. Might want to fix that.)

                                1. 2

                                  Thanks, noted! (Will push when document is next updated.)

                                1. 1

                                  tl;dr: Attaching a decorator @deco to foo’s definition is semantically equivalent to writing foo = deco(foo) after foo‘s definition. Multiple decorators attached to the same definition are applied in the reverse order in which they appear in the program text. The consequences of these two facts are exactly what you would expect if you already know the remainder of Python’s syntax and semantics.

                                  1. 1

                                    True, but the article also makes the (harder!) case that using decorators in “creative” ways may not actually be a bad idea in all cases. I found it worth reading for that reason.

                                    1. 1

                                      The article doesn’t make a very good case. The most “creative” snippets (22 and 23) are also the ugliest ones.

                                      1. 2

                                        One good example of a “creative” decorator is in the contextlib package: @contextmanager takes a function and returns a callable object.

                                  1. 4

                                    Pretty unpleasant results - often-inconsistent behavior makes it hard to even define “performance after warmup”, and lots of measurements end up finding that the “steady state” is either unsteady or worse than the startup behavior.

                                    Nice, and quite thorough, work!

                                    1. 2

                                      Thanks :)

                                    1. 1

                                      Is that company using OpenBSD for any of their products? They seem to be working on some innovative phone features, but it’s not clear (to me) what the underlying OS is.

                                      Would be pretty amazing though, if it was based on OpenBSD.

                                      1. 5

                                        No idea. But note that Android borrows big chunks of OpenBSD libc for bionic, for instance; it’s entirely possible to be grateful to OpenBSD without using full OpenBSD.

                                        1. 3

                                          They might also rely on it internally.

                                        1. 7

                                          A summary of some of what I found during my research. Interestingly, the hardware engineer that taught me a lot about subversion based on his own experience doing and countering it showed up again on Schneier’s blog. I told him to prove his identity with an example of analog subversion. His reply has nice examples of how easy it is to slip something through with no hope of verifying that stuff with any simple or cheap method:

                                          https://www.schneier.com/blog/archives/2017/08/nsa_collects_ms.html#c6757659

                                          I mean, it’s estimated there’s only around 2,000 engineers world-wide that understand analog enough for high-end ASIC’s. It’s also a black art among the rest with all kinds of tricks going back decades. So, even the nodes you can review might have tricks built into them a talented attacker can use to extract keys. We’ve been seeing mini-examples of that with side channel work on things like power analysis.

                                          1. 2

                                            Wow, this is fascinating stuff and something I don’t see discussed nearly enough. Thanks for sharing your research!

                                            I am hoping for mini-fabs (if I’m using that term correctly) so that we can decentralize chip design and manufacturing. Everyone should be able to print their CPUs locally. Any hope of that anytime soon?

                                            1. 2

                                              Mapper is a company you want to watch here.

                                              (For values of “everyone” and “locally” in the “couple millions of euro’s” range, IIRC.)

                                              1. 1

                                                That would probably be this:

                                                http://www.sematech.org/meetings/archives/litho/forum/20040128/presentations/29_CPM_Kruit_Mapper.pdf

                                                Thanks for the tip! That looks nice. Especially if they can pull off 10 wafers per hour low cost at 45nm. The technical details are also a good example of why this stuff might be mind-bogglingly hard to verify as I just wrote in the other comment here. So many tech together from MEMS to ASIC’s to X-Rays to make this stuff work.

                                              2. 2

                                                It’s ridiculously hard science and tech. The amount of money, labor, and PhD’s that go into each process node or set of advances is mind-boggling. They have patents on most of it. The barrier to entry is high. The simplest setup is tech that directly writes the chip onto the wafers without steppers or anything. eASIC uses eBeam Workstations for that sort of thing. Their prototyping runs… a loss leader so numbers might be off… is $50-60k for around 50 chips. The machines themselves are very expensive. Only so many companies that make machines that can do stuff like this.

                                                There was a fab in Europe I have in my bookmarks somewhere that operated solely with such machines. Gave rapid, turn-around time. Went out of business I think. Tough market. However, shows that groups (eg Universities or businesses) could partner together to invest in local companies doing that with specific gear. The trick is then that the supplier of thing printing or thing verifying the chips might be subverted or malicious. Tech is so complex it might be too hard to verify that’s not the case.

                                                So, it’s an open, expensive, and complex problem if you want chips that are efficient. Playing shell games hiding what equipment and fabs are in use for each run was a temporary solution I came up with. Also, doing a high-performance, massive FPGA that we map other stuff on. It gets periodically checked by ChipWorks and other firms.

                                            1. 1

                                              WTF? You have to sign in to read medium articles now? Do they think this will make me read more articles? Sigh, another domain for the shit list.

                                              (Nobody else complaining out of politeness? Or you all signed up already? Or did I just win the A/B lottery?)

                                              (So it seems to come and go. When I’m “lucky”, it says “you’ve already read one article this month. Sign in to read more. Sign in with Google. Sign in with Facebook. Sign in…” but there’s no way to avoid signing in. Switch browsers, no popup.)

                                              1. 4

                                                I’m for this change, it will make it much easier to not read Medium.

                                                1. 1

                                                  I’m not signed in, but I remember that Medium bugged be once to log in. I do believe that I had the option to choose “go away and don’t bug me again”.

                                                  1. 1

                                                    It doesn’t ask me to sign in (Safari on iPhone), FWIW.

                                                    1. 1

                                                      Works for me on mobile

                                                      1. 1

                                                        I’m on desktop Edge. It’s not asking me to sign in. Perhaps it knows you have an account? Try clearing your cookies.

                                                      1. 1

                                                        Gliffy. Not recommended.

                                                        1. 5

                                                          I’m a little disappointed that this “critical vulnerability” is just a local side channel attack that requires an attacker to have access to run arbitrary code on your system. Furthermore, the attack seems to require the victim process to use shared memory that the attacker can flush from cache..

                                                          That said, js + wasm look worse and worse in light of local side channel attacks. Maybe one day someone will weaponize them to both detect interesting events (use of private keys?) and gather & leak info about them. And pledge & privileges will not help.

                                                          1. 4

                                                            Yes; it’s good work, but this article way over-hypes it.

                                                            1. 2

                                                              The article indicates keys can be leaked across VMs - plenty of people are running on shared hardware, and they’re vulnerable to a remote attack, no?

                                                              1. 4

                                                                I guess it depends on your definition of remote attack. Yes, if you run your code on some shared host with a hypervisor that snoops your memory, and an attacker can run his code on that same host, I guess you might consider that attack “remote.”

                                                                But to me they are all on the same system, and this is why I’m just a little disgusted with VMs. They are all too cheap and convenient for people to even consider the risks of running their applications on the same system with other unknown users.

                                                                Think about it – a headline like “this attack steals your keys across VMs!” is sure to grab your attention. But what are you actually doing with these private keys? Surely something that should be kept private or secret!

                                                                Yet, unless all your application logic is designed to run in constant time with special attention to make every page unique, private information is at risk even if the keys are not compromised. Focusing on the keys and thinking the application is safe if they have carefully implemented crypto that isn’t suspectible to side channel attacks, people miss the forest for that single tree. Everything you do could be suspectible to information leakage via side channel attacks unless you’re careful about it. Keys are an obviously interesting target, but they are just the tip of the iceberg.

                                                                It would be nice if all VPS providers disclosed whether they’re snooping you or not. Apart from that, there ought to be some mitigation available (e.g. randomized builds, random junk on allocated pages, in paddings, etc.). But if everyone used these, there’s not much point in snooping to begin with. Maybe people should just stop sharing memory across VPSen to begin with.

                                                                Of course that would make it a little less cheap as memory requirements increase. It’s the price you pay…

                                                                1. 2

                                                                  But to me they are all on the same system, and this is why I’m just a little disgusted with VMs

                                                                  I can’t agree more - these attacks will only become more sophisticated and pervasive as we move more into shared resources.

                                                            1. 5

                                                              This is pretty interesting, TEMPEST omg, all that, but… questionable choice of target. They start by mentioning that this is entirely feasible against a network encryption appliance, but then they target some weird underpowered FPGA thing? Their target, as I understand it, is a software T-table implementation (which has other side channel leaks as well). But a real network appliance would be using a hardware implementation, no? Can you demo this attack against some more common hardware, like a MacBook, which would be using AES-NI on the CPU?

                                                              1. 4

                                                                I think we did mix too many attack models, especially since we/I tried to keep the paper readable for a general technical audience (which made it hard to concisely define these things). The following are indeed two distinct points:

                                                                • The “network encryption appliance” scenario is intended to show that many-trace chosen-input attacks are feasible in at least one relevant(-to-us) threat model.

                                                                • As discussed in https://news.ycombinator.com/item?id=14618916, “the contribution of this work is mostly in showing that you can break realistic-but-not-great implementations very quickly, cheaply, and without needing to open most enclosures.” We attack a MicroSemi SmartFusion 2’s ARM core (arguably a “weird underpowered FPGA thing”), a Xilinx Zynq’s ARM core (not a bad model for an IoT-ish device), and a naive hardware implementation (that mostly didn’t make it into the blog). The internship was mostly run on what one of our FPGA experts had lying on his desk. ;-)

                                                                A specialized network crypto definitely needs (and has) a better crypto core than the “realistic-but-not-great” cores we attacked here. (At least, ours do. No promises about today’s model of cheap Linux router. ;-) )

                                                                1. 2

                                                                  Oh, nice, thanks for clarifying. Good work.

                                                              1. 7

                                                                Once again, this shows up despite evidence to the contrary. The comparison to NASA is ridiculous. That process is so ridiculously slow and expensive that other high-assurance projects compare themselves to it regularly in both defect rate and cost showing how unnecessary it is. You’ll see tagline “compared to the Space Shuttle’s… blah blah.” Altran/Praxis is an example that supplies nearly defect-free software for a 50% premium that doesn’t take hundreds of people to write. Their unique aspects are using good requirements-gathering, Z specs just to catch English or interface inconsistencies, and Ada + SPARK Ada to prevent boatloads of implementation flaws. Before that, Cleanroom Methodology got quick time to market with anywhere from less cost to 30% more. Low since it knocks problems out early when they’re cheap. Similarly with Fagan Inspection Process. LOCK project for secure computing at highest levels of rigor was 30-40% premium. You’re talking 1-2 extra developers on a 10+ team with tooling that cost similar to existing tooling. Some recent ones are using Haskell with QuickCheck, Ocaml, or Prolog for reducing spec-to-implementation incompatibilities or implementation errors.

                                                                So, this claim that it cost so much to knock out lots of problems is false from the start. The Hypothesis tool is interesting. Python programmers should certainly try it. Whereas, methods like Cleanroom from the 80’s knocked out most defects (esp user-facing) from the start often on first try and sometimes without code execution by developers (obsolete but impressive requirement). I’m sure modern tradeoffs with memory-safe languages, interface checks, and testing tools could do even more even faster given work like Altran Praxis and Galois Inc. One person I read a while back even combined Python and Cleanroom for advantages of both.

                                                                So, the author certainly can argue that his tool will find problems easily in an environment where good QA isn’t supported. It might even supplement good QA. That you need to have NASA budget to get near their error rate is a myth. The only thing consistently in jeopardy for increasing assurance is time-to-market. That’s why I’ve been writing posts about methods that knock out tons of errors without taking much time or effort. High elimination of defects while low wait for delivery. Totally, different picture than CMM whatever processes.

                                                                1. 3

                                                                  Thank you for bringing up Cleanroom Methodology. I had never heard of this before and the high-level wikipedia entry makes me think that some of the tenets are basically the good parts of agile and TDD but without the bullshit. Do you have any suggestions for reading about Cleanroom to get a better feel for it?

                                                                  1. 2

                                                                    It took a while to find a good intro since resources I speak from are paywalled in ACM/IEEE & I could find no training guides. The good intro I found said that was on purpose: IBM forced people to learn by paying them at events since it was a competitive advantage and money-maker to them. Similar to them keeping PL/S language secret & squashing a publication with lawyers. The best page on Cleanroom from someone who went to that training is here:

                                                                    http://infohost.nmt.edu/~al/cseet-paper.html

                                                                    Note: I submitted that here 5 months ago where it got 11 upvotes & no comments. Sad given it’s something that should really provoke discussion & experimentation on software forums everywhere.

                                                                    Dr Dobbs did a write-up on it showing the more formalized aspects:

                                                                    http://www.drdobbs.com/architecture-and-design/cleanroom-software-engineering/184405405

                                                                    Good guess on similarity to agile and TDD: I used to tell their zealots they were largely reinventing the Cleanroom wheel with less quality. The basic method is decomposition of high-level specs into functions with a constrained way of expressing them and annotating intended behavior that makes verification easy. This is done iteratively as in Spiral and Agile. A verification team systematically analyzes the code for problems both in meaning & coding itself. That requires limiting programming constructs used & how program is expressed to make that tractable. The testing is usage-based testing created from simulations of how customers will use the software or specific features. The clever idea being it’s better to leave in 10 bugs they never experience in production than even 1 they see. User’s positive perception increasing software’s value is a business argument for Cleanroom. Finally, after enough software is produced by a team, Mills theorized the defect rate should fall in a range that could be statistically certified. This number could be used (was used) in warranties that rated software at a specific, defect rate. It could also be used to improve weak spots of developers' skill areas.

                                                                    Now for some meta stuff I learned. First, the paywalled sources of early use showed the method worked. The defect rate was super low on Mills' teams. The other effect that’s unusual in QA is it dropped the defect rate a lot on first try. That shows it captures intrinsic aspects of software correctness but those should be obvious to yall from my description. They didn’t allow developers to compile & test their own code even though many admitted they did anyway before submitting to avoid embarrassing failures. Although sort of thought unnecessary, I found one source say the real reason for no compiles was computer time was scarce enough in the 1980’s that compiling less programs let them get more actual work done. We can drop “don’t compile & test it” since we know doing that is beneficial. Although PSP/TSP shows metrics can improve programmers, I’m currently for dropping any claim of statistical, final, defect rate on the software being stated to customers unless team keeps doing similar kinds of software. Being great at one domain doesn’t mean they’ll be great at another & vice versa. The metrics can be shown as a differentiator or used for warranties, though, in that the company promises to fix at least a certain amount on the house. When picking the rate to use, one might go with either the current median or the highest ever encountered depending on how greedy or altruistic. ;)

                                                                    Also, although CASE tools were made for it, the Cleanroom method could be embedded in a high-level programming language much like people do functional programming in C or C++ by only using specific, language features in specific ways. I thought this long ago with the link I just shared confirming it: Stavely’s students did this. I also believe that combining Cleanroom with functional programming, Design-by-Contract, assertion-based testing, and random testing could lead to some of highest productivity and quality achieved with the method. They’d be working at a higher level with languages intended to work with functional composition. Right tool for the job. Note that it doesn’t have to be top-down, though, so much as there be a connected chain of functions between high-level intent and low-level modules at point software is distributed.

                                                                    There’s still exploration to do on intended functions vs Design-by-Contract-style assertions. We do one, the other, both, intended functions in the assertions, what? (shrugs) One thing I’m sure on at least to start with is making them do human verification before testing to drill into their brains the patterns of what correct and incorrect programs look like along with systematic way of looking at them. None of that “I glanced and thought it looked right” bullshit people call code review these days. Also, prior work in high-assurance on formal specifications showed that they found more defects modifying the specification for use in a prover than using the prover itself. I intuitively know there’s a tie-in to that here where Stavely points out how they had to learn to simplify & properly structure their programs for easy, human verification. It’s that mental process or habit that I’m trying to embed in their mind by not letting them throw their programs at testing tools before human verification. Like Agile showed, people will learn to spot patterns of where trouble is likely to show up in a code base & know to eliminate it immediately.

                                                                  2. 3

                                                                    Your comment appears to support the thesis of the article. “Make it cheaper to find bugs.” Hypothesis is a Python version of Haskell’s QuickCheck, with more functionality than the original QuickCheck.

                                                                    1. 2

                                                                      @nickpsecurity wrote:

                                                                      The comparison to NASA is ridiculous. That process is so ridiculously slow and expensive that other high-assurance projects compare themselves to it regularly in both defect rate and cost showing how unnecessary it is.

                                                                      I’m not sure if I misunderstood your comment here, but I believe the author agrees with you. He specifically wrote:

                                                                      Also, if you look at the NASA development process you will probably conclude that we can’t do that. It’s orders of magnitude more work than we ever put into software development. It’s process heavy, laborious, and does not adapt well to changing requirements or tight deadlines.

                                                                      I’m not familiar with Cleanroom, Altran, or Praxis, but it sounds like to me the author is advocating the use of tools and techniques similar to those to make it easier (or “cheaper”) to write correct-enough software than it is with a NASA-style approach.

                                                                      He didn’t specifically acknowledge those tools, and perhaps that’s what you’re reacting to, but I didn’t read him as saying “without Hypothesis and specifically Hypothesis you need a NASA-level effort to get anything right!” He even wrote:

                                                                      And so this is the lever we get to pull to change the world: If you want better software, make or find tools that reduce the effort of finding bugs.

                                                                      Obviously I think Hypothesis is an example of this, but it’s neither the only one nor the only one you need. Better monitoring is another. Code review processes. Static analysis. Improved communication. There are many more.

                                                                      1. 2

                                                                        The author disagreed with my position before on basis that most developers won’t do QA at all or use anything but a near-pushbutton tool. Hypothesis was his solution. So I countered that as bringing them methods like Cleanroom would eliminate more defects. They can add Hypothesis to that, too.

                                                                        Also, the author is misleading people by making them think low-defect software has a typical cost or time-to-market of NASA’s. They’re such an outlier people probably shouldn’t even mention them. He’d have been better off referring to formal methods in industry where at least refinement proofs support his position. Yet, I could still counter it if we’re talking about lightweight methods like model-checkers or formal specs since those surveyed usually say time spent is lower than time saved during debugging.

                                                                        So, there was more than this post in isolation I was responding to.

                                                                        1. 2

                                                                          Ah, I understand. Thanks for elaborating.

                                                                      2. 2

                                                                        You’re mostly right, but Altran / Praxis / Galois do have the advantage of being staffed by people who especially hate bugs (I’d expect). From personal experience, that alone helps a lot.

                                                                        That said, Cleanroom / Fagan / etc. have been used widely enough - and Praxis etc. claim sufficiently spectacular results - that there is definitely something there. Do you happen to be aware of studies looking at the more junior end of developers?

                                                                        1. 1

                                                                          The reply I just posted to apy in this thread has a lot of detail on Cleanroom applied to people with no experience at all. Check it first. Defect rates stayed under 10 per 1,000 lines of code if they were familiar with the programming language. Data on the Eiffel Method and Design-by-Contract was always positive when people were doing real specs. One experiment on stronger specs (not proof though) caught more problems. However, industry data indicated many of them weren’t doing anything past null checks since mgmt didn’t push them on it. The Abstract, State Machine method was used to formalize all kinds of stuff whose teams must have had a mix of skill levels. Always succeeded in knocking out spec errors that would’ve been costly or impossible to fix once some of those were deployed (esp industry standards). NIST data indicated combinational testing at 3-way knocked out over 90+% of errors with them detecting nothing after 6-way. Each, simple, inexpensive method got good results in any case studies. Combining the simple ones on developer side w/ semi-automatic, test generators & fuzzing running overnight should arguably get high quality at reasonable, cost-benefit ratio given above data. My hypothesis has to be tested of course but prior data gives me a lot of confidence in it. At worst, some person-hours will have been wasted overdoing it a bit that were paid for by those saved during debugging if we’re talking inexperienced programmers. Those experimenting can then just dial-down a bit on the methods used to see what happens.

                                                                          I mean, just look at how reliable things like OpenVMS and AS/400 got just doing something similar to Fagan Inspection Process on design & implementation. I’ve never met an AS/400 user whose witnessed the system crash. Many used them daily for 10-20 years, too. VMS admins sometimes forgot reboot command with clusters lasting years (record was 17). They were able to keep competitive pace with industry with plenty of profit despite whatever design and quality assurance they were doing. Their decline happened for market reasons rather than development failures. I hope and believe we can use methods like I describe above to get junior developers closer to that level of quality or reliability. Probably still best to have at least one, senior dev on the team who will spot bad ideas or re-apply prior solutions.

                                                                        2. 2

                                                                          I always find your comments very interesting and insightful. Do you have any recommended readings for those outside the high-assurance field who’d like to start learning about it (and ideally start applying some of its practices in their day jobs)?

                                                                          1. 3

                                                                            Why thank you! :) I did. The problem is the info is scattered, usually specific to a subset of it, and little uptake by mainstream leads to many site owners to let their links die. I periodically go dredge up whatever I can but it’s time-consuming work. I might in near future do that again to at least find intros to field overall, examples from various categories of assurance methods, case studies in industry if I can find non-paywalled ones (almost all are…), what tools I’ve found to support it, and suggestions for improvements on any of that. I’ll just add your name on my list of people to send that to if I get around to it.

                                                                            Meanwhile, the Cleanroom reply I posted in this thread will given you a good idea of the mindset. Another that’s more rigorous is Altran/Praxis method below which combined Z, CSP, and SPARK language. There’s intros & FOSS you can Google but replace CSP with TLA+ optionally with hwayne’s tutorial. DeepSpec is cutting-edge example of “mathematically-prove everything” style of development. A few companies cheated by encoding business rules or specs into first-order logic executed in Prolog or Mercury languages. Prevents lots of mismatches & coding errors with no extra effort albeit you gotta be able to work with the notation. Eiffel’s Design-by-Contract combined with memory-safe and/or functional language would be another good cheat at getting some formal benefits without really doing formal.

                                                                            http://www.anthonyhall.org/c_by_c_secure_system.pdf

                                                                            https://deepspec.org/main

                                                                            https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf

                                                                            https://www.eiffel.com/values/design-by-contract/introduction/

                                                                        1. 7

                                                                          This is a great write-up. It goes into exactly what I had to slog through for over 10 years to get to the point I can explain what I know in IT and INFOSEC, esp esoteric stuff. It was all scattered among tens of thousands of books, papers, and articles I had to go through. I got quick at looking at abstracts & dissecting highlights from the papers of many fields. The intuition I developed sped the process up a lot. Most I haven’t fully digested because that’s difficult as the OP suggests. Yet, I’m sure based on seeing it all that much of it could’ve been summarized or introduced better to save me literally man-years of effort.

                                                                          Heck, we even occasionally get that in the form of survey papers. They often won’t serve as an introduction. Yet, an introduction combined with a good survey will give you quite the head start on where the field is, maybe some of the why, and what you might want to do. The OP overestimates the work required to do that given each sub-field might just need 1-4 experts doing both of those periodically. So, for each subfield, you just try to convince about that many to create those resources. Also, do whatever it takes to make sure the resulting publications are posted wherever newcomers are likely to see them. Each time you succeed, you enable a huge swath of people to get past a lot of research debt.

                                                                          The distilling part in general is a cultural problem that also has high amount of effort. I don’t have any suggestions on how to fix that. I think these problems with academic culture will require top-down solutions from groups controlling them and/or funding bodies. That is if you want major change instead of just small groups doing better.

                                                                          1. 3

                                                                            FWIW, IEEE S&P has a dedicated category for “SoK” papers; S&P is a fairly major conference, so that helps at least a little: https://www.ieee-security.org/TC/SP2017/cfpapers.html.

                                                                            I agree with you, but fixing this may not be that hard.

                                                                            1. 2

                                                                              Hm I haven’t heard the term SoK, but I like it. I would love to see a list of SoK papers across all subfields of computer science.

                                                                              I have a few that are good, like “Abstract machines for programming language implementation”

                                                                              https://scholar.google.com/scholar?cluster=9404775585425389399&hl=en&as_sdt=0,5

                                                                              And there are a few on MapReduce-type systems.

                                                                              1. 2

                                                                                That was a good one. Btw, you can share this research more easily if you post it in more accessible form. Preferably right to the PDF or something with easy link. Best resource is here:

                                                                                http://citeseerx.ist.psu.edu/index

                                                                                Type name into it to probably get description, metadata, and PDF link as so:

                                                                                http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.68.234&rank=1&q=abstract%20machines%20for%20programming%20language&osm=&ossid=

                                                                                Just save them, bookmark the links, etc.

                                                                              2. 2

                                                                                The final . was included in the link by accident. The correct link is

                                                                                https://www.ieee-security.org/TC/SP2017/cfpapers.html

                                                                                1. 1

                                                                                  Yeah, that’s the sort of thing I’m talking about. Each sub-field could get a lot done with just a handful of people. Btw, while trying to re-create history of high-assurance security, I did find an important summary that came from S&P where they sort of surveyed themselves & INFOSEC field:

                                                                                  https://sci-hub.cc/10.1109/SP.2010.43

                                                                                  Note: Paywalled of course… (rolls eyes) I suspect that’s part of the reason most INFOSEC people don’t know INFOSEC. They never saw the important work, techniques, case studies, and so on. Most still cant tell me what a covert channel is or how they’d find them in their favorite OS/stack.

                                                                              1. [Comment removed by author]

                                                                                1. 4
                                                                                  Lightweight notation formats

                                                                                  If you really need LaTeX, you can use something like org-mode from emacs, or any other system that lets you write in an easy format, then convert it to LaTeX.

                                                                                  Troff

                                                                                  macro packages - You can also use troff. This should be easy to get started as it is alrrady present on your machine to format man page: man 2 name is like groff -Tutf8 -man /path/to/name.1 | less. This is for ‘man’ format, but you also have other output: -Thtml, -Tpdf; and other input formats: -mm, -me, -ms … for papers, books, RFCs…

                                                                                  preprocessors - And then you can insert tables chemical/math equations and formulas, diagrams and drawings… by using preprocessors, that transform a sub-language dedicated to each kind, to the general troff language.

                                                                                  utroff - a well-documented set of macro package for a powerfull implementation of troff: heirloom doctools.

                                                                                  HTML + CSS

                                                                                  Before the web got so popular and still nowadays, HTML + CSS is more a typesetting system than anything else. We pay millions to hire developpers to can make a webapp fit into a typesetting system. We can totally use this typesetting system for typesetting.

                                                                                  All you need is a web browser, and a text editor. Hit CTRL + P and you have a high quality document made by one of the largest software project made by one of the largest IT company, all of that with a debugger that let you click on an arbitrary node of your document to see corresponding source, that you can edit to get immediate result. I do not think any other typesetting system made something as crazy as this.

                                                                                  Bonus: you do not need to learn it: you already know it.

                                                                                  1. 2

                                                                                    I’ve been wanting to switch to HTML+CSS for papers for a long time, but imo the quality of the print output from browsers is still worse then latex, and browser support for the print-oriented portion of CSS is poor.

                                                                                    It is possible to get great print output from HTML+CSS with PrinceXML, but I’m wary of becoming dependent on a very expensive proprietary software product.

                                                                                    1. 1

                                                                                      Better not be dependent on a proprietary expensive software, as you said!

                                                                                  2. 3

                                                                                    We’ve covered a few here recently that are promising (SILE being the one I’m most excited about and most interested in), and there are ways of using TeX without getting knee-deep in TeX itself (e.g. via Pandoc), but there aren’t really any systems right now that have TeX’s breadth and depth.

                                                                                    That said, if your concern is with LaTeX, as opposed to TeX, and you don’t need to work with LaTeX, I personally find ConTeXt on LuaTeX a much saner environment. Similar power to LaTeX, and obviously the same ultimate underpinning, but a shallower learning curve.

                                                                                    1. [Comment removed by author]

                                                                                      1. 1

                                                                                        XeLaTex has support for OpenType fonts installed on the system. LuaTeX has to do this via a package. Both have Unicode support.

                                                                                        1. 1

                                                                                          LuaTeX I just like because you can script in Lua instead of TeX. If you’re just using the verbatim ConTeXt or LaTeX templates, it should work similarly to any other TeX system. (Though, as ane points out below, XeTeX has better out-of-the-box OpenType support.)

                                                                                      2. 2

                                                                                        What is your exact problem? Pandoc/Markdown/Sphinx, LyX and LaTeX-kept-simple all solve (and don’t solve) different parts of this.