Schneier on Security

Nick P • January 31, 2015 1:44 PM

A BSD magazine subscription sent you an issue about a BSD. Im missing the synchronicity or weirdness. Unless it’s the timing. And for that, we must look at timing range of other issues you received to see if timing is unusual. So, is it?

Nick P • January 31, 2015 8:52 PM

@ Clive Robinson

Interesting. The best part is that it’s from WaywardGeek. He’s the CipherShed team member that responded to my post on SCM security. Pretty cool and smart guy.

Nick P • February 1, 2015 11:37 AM

re cell phones

We managed to get by for thousands of years without being reachable 24/7 by cellphone. Industrial society with telecom got by for decades. So, just take the battery out of it unless you absolutely have to be reachable. You might also select a phone where that’s easy plus a case (or pouch) that can fit both phone and battery. I just threw it in part of my briefcase or backpack. Knowing how I pick them, always plenty of compartments to choose from. 🙂

Nick P • February 1, 2015 1:44 PM

@ Wael

Oh, I agree. The point was that we have to worry about each and every part of the security scheme, including RNG. Enemies are counting on us to forget about something. For practical reasons, I advocate coming up with reusable solutions like my manual seed + CRNG option. That way, we worry once about the scheme, are done with that, and then just do a tiny bit of worrying during integration with next project. We can do this for many pieces of the problem.

@ Wael, Clive

Back to security engineering. Closest, practical thing to Clive’s prison concept are the distributed information flow tracking (DIFT) architectures. They typically tag data base on provenance (esp risky I/O) and/or type. Security features kick in if certain operations (eg pointer manipulation) happen with “tainted” data. There’s usually quite a bit of overhead and modification to various parts of the system. Then there’s this scheme.

It’s clear to readers that, although flexible about approaches, I’m mostly focusing on schemes that make leaks or code injection flat out impossible with decent performance. However, I couldn’t help but admire the pointer policy used in this scheme [but developed elsewhere]. Pointers have two tag bits: one to represent any legitimate pointers, another to represent tainted/risky data. If both bits are 1, dereferencing isn’t allowed unless a trusted program declares the data legitimate. Simple trick stops many attacks like overflows with only two bits of overhead. Nice. Their overall scheme also has nice performance, hardware dev/resource properties, and runs legacy Linux code.

What I still think is we need some talented security engineers coming up with a checklist of about every type of code injection attack (or invariant to ensure), reviewing each of these clean slate designs against the criteria, assessing the assurance of their claims, and turning that into a technical report for various stakeholders. The report might also include things such as legacy compatibility, performance hit, amount of chip modification, intellectual property rights, and so on. This could help those designing or funding chips (plus research) to focus on what has most value.

Sadly, I’ve seen little activity like this so far outside a “Survey of” paper here and there along with “related work” section of papers. Those are great papers and sections for sure. Yet, I’d like to see more detail and empirical data from people experienced in both sides of the game. Last chips standing that are also practical all get funded and brought to market somehow.

Nick P • February 1, 2015 3:51 PM

@ Figureitout

Many evaluations, arguments, and sometimes mathematical proofs have backed such architectures. Flaws were never found in some. Then, you say without evidence that such approaches are weak, hack n’ patch, and so on. Then you give an alternative setup that has those exact properties. Why the double standard?

@ Wael

“That, and Bromium. Thing is the delineation of C-v-P isn’t crystal clear (in my mind) yet — it can have a frame of reference dependency. Getting closer, though…”

That’s why I don’t like the metaphors regardless of how good they sound. The trouble they cause leads to effort wasted. Better to focus on the proposals themselves: TCB, design, security policy, security mechanisms, how they correspond, and assurance of each. Bromium I wouldn’t compare to Prison as it’s really just a Qubes-style virtualization security scheme with some AV/NIDS/HIDS type tech integrated. (My guess, that is.) It’s granularity is at practically the OS and app level. Prison architecture works at the “function” or task level across the entire system with mediation kicking in upon changes to main system state.

So, separation kernel architectures with message routers, hardware functional programming with mediation, system wide inline software monitors, DIFT/tainting… these techniques seem to fit his model better than others. One of the reasons for requiring small granularity is that it’s easier to analyze along many lines. Virtualization schemes usually have whole OS’s and app’s worth of data moving around. At best, as with Flicker and SKPP, we can argue the properties of an isolate app outside the main systems. That’s useful but nothing like claims by clean slate or prison architectures.

“we’ll not only “imprison” data, but components, pieces of code, and subsystems as well… ”

Sort of. Many schemes are isolation based. The SAFE-style tagging schemes seem to be about tying together a type of data with permitted operations. So, it’s more about permissible operations than really imprisoning things. The system architect could make a system with no security at all. Example: a Python interpreter with access to system routines/data and a web front end for user submitted scripts. The interpreter won’t be compromised, but it can compromise everything else. So, the proper concept for security architectures is a superset of all of it: control of data or operations to enforce a specific requirement.

” @Clive Robinson’s voting, predictive, and probabilistic security schemes are a few possibilities that haven’t been detailed to an implementable ilevel as of yet; some elements are implemented today, but not the whole idea. ”

There could definitely be work in that area. Fortunately, recovery-oriented architectures, availability architectures, and security through diversity work keeps innovating on such techniques. Byzantine failure research alone has reinvented and revised the concepts repeatedly. So, I’m sure we’ll get to read (and maybe use) plenty more good work in that area in the future. In some*, the voter itself is distributed and attempted to be fail safe. I’d especially like to see more research like that.

• Note: That was just the first search result and is for illustration of the principle only.

“This is a moving target (expanding.) At what point will we be able to say: Here is a complete list of injection attacks?”

There’s two ways of doing it: argue that it stops specific attack vectors; show that it, in all cases, maintains an invariant that makes attack vectors irrelevant. As you said, the first is a “moving target” or as I say a “perpetual backdoor generating machine.” Second strategy is what I advocate where possible with first just a check against it or an interim approach to problems not solved by strong methods yet.

The simplest example is a control flow integrity scheme where every jump is mediated against a whitelist of allowed jumps. Come up with a hundred types of data to use or ways to put it in the jump. Still fail in the attack because the jump doesn’t meet the criteria. Another is capability hardware that treats pointers as special, limits their memory access, restricts their creation to approved processes, and enforces security policies (eg read/write/execute/propagation) on them. Many key attacks smash or abuse pointers directly, which is provably impossible in such a system. In each of these systems, attackers will likely have to string a bunch of flaws together in a smart combination to breach the system. Much like Chrome sandbox attackers often do. Strong mechanisms are developed over time to give attackers more duck tape, shackles, scrutiny, and so on.

“but it has to do with money, academia, and industry — and “smoke and mirrors” as well as “dog and pony shows”, etc…”

I’ll take a guess: all three are better off creating rather than reviewing things. We know industry doesn’t like security, much less rigorous evaluations. They make more money by promoting faux security and reducing the real thing. Easy. Academia, on other hand, does regularly evaluate others’ work if only because schools seem to require it. Why not regular and thorough examinations of a whole subfield, though? My hypothesis is that they get more fame, citations, and I.P. licensing fees by creating more usable results. Creating significantly less tech to review existing tech detracts from all those and so it’s not in their incentive to do that.

I mean, I’ve been doing it for years. Result: no splendid office, salary, or academic title. Academics’ response might be that simple. It might be other things. Open for debate like you said.

re your old advice

You said the best approach will probably be the cheapest to implement. I’ve kept it in consideration. One thing I’ve noticed, more intuitively than measured, is that academics have come up with a great many ways to enforce strong security with seemingly similar amounts of effort. Might indicate that development cost is similar across projects that don’t have to make substantial modifications to, say, whole CPU’s. If so, then the cost model is that being able to afford to develop a solution at all = being able to afford to develop a really good one. That’s some good news in a field without much of it.

Now, the unit costs are a totally different story. Ignoring process node costs, the extra cost of a secure chip is how much stuff you put in the chip (individual chip cost) and how many chips are needed to make up for performance disadvantage. Naturally, the less a scheme does on the chip, the cheaper the unit cost will be. The optimization here is (1) to put an upper bound on price based off what market will usually pay for semi-premium stuff, (2) determine which approaches can be made for under that amount, and (3) pick the best of them.

It’s helpful that the individual papers offer plenty of measurements on performance and chip area. Some even do power consumption. Plenty to draw on.

Nick P • February 1, 2015 11:08 PM

@ Wael

With CFI, the mediation can happen at many levels. The strongest schemes do it at the hardware level with actual circuitry running parallel with processor. Examples are a list of permissable jumps created at compile time enforced by processor checks during execution or tagged memory that keeps data from overwriting pointers. Another scheme disallows jumps by default, passes the attempt as an exception to a trusted software process, and stores permitted jumps in a cache for faster lookups. Many ways to do it. All enforce the invariant of “control flow works as it’s supposed to” rather than “let’s hope we stop tactics X, Y, and Z from hitting unprotected control flow.”

“I had this request before! Remember? I more or less agree with the rest of what you said.”

I see what you mean. Looking back at it, that particular quote is horrifically self-defeating with the use of the word monitoring. My bad. Might have taken a while to say but I said it. 😉

“The image I have of you is that of a researcher sitting in a cube working on a dissertation, is that close? Shed some light on what you do :)”

Far from it. I’ve previously said my work is a shit job outside IT that barely pays the bills. I just do whatever my company needs me to do. The duties range from blue collar to white collar to security to whatever. I’d rather be doing what you described minus the cubicle: I’d never work in a cubicle due to detrimental effect on the mind. I’d work in a modified janitorial closet before a cubicle if only for the privacy and lack of interruptions. Well, the boss banging on the door of an echo chamber while I’m in deep thought could be pants-shittingly startling. Might not be such a good spot… Roof maybe?

Of course, we both know you’d just like to get closer to knowing as much about my career history as I know about yours. 😛

@ Buck

“and please pardon my metaphor here”

HA!

@ Clive Robinson

The bit problem is a tradeoff. We can learn a lot by looking at the ones that go overkill on it: SAFE and CHERI. There’s still more than enough memory left over in these. More lightweight systems can squeeze a ton of protection out of 2-3 bits. There’s also systems that effectively stretch the bits with encoding. So, this issue does have an impact but far from a deal ender.

“More importantly do you have tags for char,int,long long etc and do you also have a tag for if they are signed or not, also what about null data or unset values? ”

You don’t need to know all of that. Almost all injection attacks target pointers, arrays, key memory areas, and so on. They need this to function. So, your goal is really to create a scheme that maintains protection of such things. The oldest tagging systems often worked in conjunction with memory protection (eg segments) to achieve that. Some just protected things like pointers, while others (eg System/38) had rules for high level objects like stacks. So, realistically, you’re more likely looking at scalar data vs array with bounds info vs pointer vs piece of code vs I/O object. Things like that have sufficed so far.

Note: SAFE is one that has an extra 32-bits in the tag with support for near arbitrary policies with user-defined types. Operations fail by default, results sent to a trusted handler in software, and permitted ops’ type rules get put into the cache. Their recent paper showed them running four very different security policies simulatenously. The performance impact on their alpha quality prototype was significant, but actually acceptable for many applications.

“On balance I find the lack of tagging less secure but more efficient as well as more programer friendly thus market friendly than tagged systems which with a very limited and fixed data type set are more secure. ”

CHERI already runs FreeBSD, a few others run Linux, and SAFE could easily be targeted by Java. The security vs legacy tradeoff is adjustable incrementally. Sounds pretty market friendly to me.

” The trade off is complex but I just don’t think the general computing market is going to accept the significant limitations of tagging for what will be seen as a marginal increase in security.”

Good tagging schemes offer a great increase in security up to the total prevention of entire classes of code injection. The part about the tradeoffs and market acceptance are true, though.

” especially as I suspect the pragmatic result will be a hybrid solution.”

That’s very possible.

Nick P • February 1, 2015 11:31 PM

@ Buck

Interesting to re-read what I wrote there so long ago. Found this off-topic remark in response to a government conference:

“The real nuggets to take home from what I read are these: NSA is relying on COTS for sensitive information; NSA hopes to rely entirely on COTS; NSA strongly promotes TPM and TNE in COTS products; NSA is leveraging trusted software on untrustworthy processors; NSA hopes to reduce accreditation time for these untrustworthy COTS components. To be honest, I’m not really comfortable with any of these points. Brian Snow’s work made me think the NSA was making progress in the right direction. Now I know better.”

Post-Snowden, still true and for more obvious reasons. By 2010, I had a firm grasp on all their varieties of bullshit. Although, I still questioned at the time whether it was intentional subversion or incompetence related to politics/funding. Clive’s remarks indicated he was unsure and leaning toward the latter as well. One value of the leaks is that they cleared that up for us: subversion for surveillance state, not failures of the Idiocracy. Always love tying up loose ends in long-running investigations. 😉

Nick P • February 2, 2015 1:39 AM

@ Wael

When I saw “smart pipe” in the URL I knew what kind of shit I was about to see. But how you got our base SDK I’m not sure. I think we have a leak we need to plug. Maybe we shouldn’t have those “penetration” testers attacking our “pipes.” Who knew the rain of shit that could fall on us for accepting such a contract!?

Note: I needed the laugh after watching Kill The Messenger. I appreciate the short-lived relief from reality.

Nick P • February 2, 2015 10:42 AM

@ Clive Robinson

Smartphones aren’t thin clients. Thin clients perform almost no computation locally: merely provide an interface (eg web browser) to a computer that does. Smartphones have so much functionality they can replace desktops for many use cases. The only real difference is number of I/O ports and price-performance ratio.

re neuromorphic chips

Something I’ve looked forward to for a long time. The applications should be interesting. Far as security, these architectures would be less secure due to inherent flexibility and no visibility into its internal model. There have been security applications of neural networks in the monitoring domain. Not sure what value they have past that.

Nick P • February 2, 2015 10:40 PM

@ Nate

Dude, that was 2010 when NSA’s image was still legit and Google just got hit with a big cyberattack by Chinese government. It was a decent option from a company’s perspective to get help from a top electronic espionage organization that regularly battles with China and is paid by taxpayers rather than Google’s wallet. Today, they’d be less likely to make the same move.

Nick P • February 2, 2015 11:29 PM

@ Nate

Night and day my friend. That’s the difference in perspective of NSA pre- and post-Snowden.

Nick P • February 3, 2015 12:34 PM

@ Figureitout

tedu’s article says you have to know what to implement and then implement it right. Safer languages are for the second part. Then, you picked an article where a guy works his ass off to make a failing construct in Rust. He then admits “no true rust programmer would ever write a program like that.” That’s when the reader with a brain clicks the little x to not waste more time.

Note: Funny the next article is Ada because there’s an article out there showing Ada use would’ve prevented Heartbleed with bounds checking.

The Ada article you picked shows a subtle flaw in the type system where a number of things have to be combined for it to fail. A so-called Heisenbug that’s extremely hard to spot in advance or detect while testing a compiler. I’d forgive any language author for such a slipup. That you use that one subtle error as evidence against Ada while ignoring its many successes undermines your argument. It was also empirically shown to be 1.37 times more cost effective than C with 5.9 times better defect rate overall. Also outdid C++ in both categories although closer to 2x less errors than 5x.

Feel free to keep trying to find selective, anecdotal, and even highly made up (tedu) evidence to argue that type or memory safety doesn’t reduce vulnerability count. I’m sure some individual might buy into it, write some C software, get it widely adopted, and make NSA hackers smile at their new boxes. 😉

@ Wael

That’s what the guy said in the article he linked to: gotta know the feature and implement it properly. His Heartbleed bug intentionally avoids implementing the feature. Has nothign to do with language arguments except for trollish ones saying “X prevents all problems!”

@ Clive Robinson

There is a bit of evolution. However, most of them are rehashes of the same thing: pointer abuse, buffer abuse, overpriveleged OS mechanism, covert channel, and so on. There are tools that totally prevent these and some that detect them reliably. We just need to use the tools. Past that, there’s containment (“Inevitability of Failure”) and recovery mechanisms. Plus, developing new defenses for each attacker advance.

Far as nets, it might become another tool in the toolbox. The fields of static analysis, dynamic analysis, and type systems already have tools to knock out almost every major error in a deterministic way. A number have mathematical proofs of their method, as well. So, I promote putting money into further work on those and integrating them with developer tools. Black boxes with significant error rates, no understanding of internal workings, and huge training sets would be a step backward for program analysis tools imho.

“NSA et al throwing lots of money at the problem in order to rapidly find new attack vectors to add to their arsenals and thus stay ahead of who ever the “Orwellian enemy of the day” is.”

This part I agree with. It’s probably what they’re doing. The defenders are barely trying to find problems in their code. The attackers have plenty of labor and tool money. So, their odds of discovering something are better. It wouldn’t surprise me if NSA tried using a neural net for finding vulnerabilities in binary code. Neural net to find it, deterministic tool to generate exploit.

Nick P • February 4, 2015 12:03 PM

@ name.withheld

The question is what tools and at what quality they are using. Now I have been aware of insidious methods for some time now. 😉 It’s why I advocate building software with tools that eliminate such things by design. Their labor and incentives are a force multiplier defenders using manual methods will never keep up with except for rare, limited cases (eg qmail, GPG).

Btw, since you helped review a tool, here’s a gift or two to help with your various embedded efforts. Galois stays kicking ass in practical and assured development. Those might benefit your own work.

@ Figureitout

“That’s something Nick P seems to have a problem coming to terms w/”

Nah, that’s a lie your telling repeatedly to justify your claims. My security framework has a bunch of human-centered activities with implementation being just one part of it. All the activities must be performed correctly. Then, I add that some languages make the implementation safer and you start talking like the programmer should worry about a million things unnecessarily instead. You also write as if I haven’t said anything about the other things. All quite deceptive to support your view that weak tools and strong tools are the same. Or recently…

“Code-cutting is only ok when you reach a certain level”

…that anyone using strong tools is a code cutter. On contrare, why would you force a master craftsman to waste time with subpar tools? You’re really saying Wirth’s Oberon systems were code cutting because he used a safe language? MULTICS and 99.999% uptime mainframes are code cutting because they used PL/I-style languages? The SPARK implementation of Bruce’s Skein algorithm is code cutting compared to the (flawed) C version? Compared to these, all these C/C++ apps and Linux systems look positively hacked together with all the maintenance and security troubles one would expect.

“Oh really, and you couldn’t find it in your link farm?”

I found three from the 90’s. They’re all dead now. Common problem with things from the Old Web. Wayback can only keep up with so much. Personally, I’d rather do new studies on the modern tools to see where they’re at. New C++ standard borrows a bit from Ada and even functional programming. Should improve quality & productivity over previous standard. Ada 2012 design by contract, which Eiffel already proved out, will make it kick C++’s ass in software maintenance and preventing interface issues.

Note: That people often download and fail to compile C/C++ applications without hitting forums with questions says plenty about that toolset. Rarely have that experience in type safe, better integrated languages. (Not including Java for this claim…) Those apps just run.

“Abstracting away memory problems that are the programmers’ responsibility will in due time mean that eventually programmers won’t even know how to check for memory errors or even know when it’s happening.”

So, given that claim, the mainstreaming of things like Java and PHP means there should be nobody right now that knows that stuff. And yet there are more people using C/C++ and doing low-level coding now than ever. Reason: people choose what they want to work on, with what tools, and so on. Plenty choose low level, memory managed stuff. Another false claim you use to push for a lack of memory safety for majority of apps.

“Oh so many successes, how much exposure has Ada really had to attackers? Probably mostly the ones that’ll be “in & out” anyway.”

No, not the riff raff out in the wild and I wouldn’t feel better if it survived such low caliber people. Professionals have used it for decades, though, in safety- and security-critical applications. A high assurance A1-class runtime was also built a long time ago. That’s the level NSA pentesters often gave up on and that runtime secured arbitrary Ada programs. So, there’s your upper bound on what it can do if you design it that way. Whereas, C/C++ “sandboxes” on C/C++ “hardened OS’s” continue to be smashed in more and more clever ways [that often don’t apply to safer languages].

Note: Main risk is the complex compiler. I’d build a tool to convert Ada to a C subset that preserved its safety checks. Then, run that through CompCert. Compilers need more security analysis, though. Runtimes get plenty of effort in quality improvement thanks to DO-178B, etc.

“Oh “empirically shown”, shove it. I want real field testing, not some fruity theoretical ”

Now I know you’re so biased you’re not even trying to think or check sources. In that paper & programming in general, empirical evidence means the results of work in the field: watching people use the tools for similar projects, measure the results, and comparing. Every study showed Ada programmers outperforming C/C++ programmers in productivity and defect count. This included when they were C/C++ programmers that just learned Ada. Says a lot. Likewise, Coverity’s automated defect hunting tools show that Python code is currently the safest in the entire industry due to good language design. Similar for LISP and even Java [in hands of at least average programmers].

It would make sense if people still used C with FFI for absolutely lowest level or most performance critical algorithms of the system. LISPers, Smalltalk, functional programmers, etc often do. Yet, the empirical evidence against it in general would argue for using the other stuff wherever possible. Given the better languages have been used to write OS’s and mission critical applications, I doubt the person developing the next BitTorrent client or web app really has much excuse to use inferior tools.

Conclusion

Using good tools to do better work isn’t dumb: it’s common sense in most industries. Even mainstream IT has learned this lesson. Sooner INFOSEC developers do, sooner we can get more robust stuff out there.

re other links

Shen
“Huh, how about that? They didn’t like the type system and tried to actively “break out of it”.”

Glad you noticed my actual point that time. A type system so powerful, yet too unusable for even most mathematicians. How to fix that (the mathematicians’ education and/or type system) is an open question. Yet, I figured more openminded people with a math background might have clever ideas for how to use or improve such a powerful type system. This is what happened with provers in general. Started out as horrible, several hundred page long, handwritten monstrosities. Now, we have compositional, machine checked proofs and lightweight, automated tools like SPARK. Shen might have potential given a lot of work.

“That paper sucked (clicked x-box), dumbass smiley graphics “Carl playing Cmdr”.”

In other words: “I neither liked the author’s presentation style nor understood enough about LISP programming to assess his work. I have nothing further to add.”

“Why compile to C code? Why not straight assembly?”

Because C is a virus that spread to about every platform and toolchain. There’s more work on C compilers than anything else. So, the easiest route to get from a HLL to arbitrary assembler is to compile to a safe, effecient C representation. Usually includes the runtime, bounds-checks, etc. I used to do this with type-safe BASIC and even LISP. Matter of fact, Chicken Scheme compiles to C with some of the best speed in the industry.

Coding directly in it in general is a sin given modern tools. Leveraging its multi-decade-optimized toolchain in a safe way is smart if one has limited development resources. Many do both: one to C for portability and one to a few native targets for hopefully better results.

Don’t worry, though: LLVM bytecode is catching up as the new cross-platform assembler. There’s already a formal semantics for it in the works. The safest language out there, Haskell, was already integrated with it. It’s a major experimentation hub for optimization, program safety, and so on. Apple’s dependence on it ensures it gets funding and improvements. Will only get better.

“When all the Lispy type systems get some real exposure”

They did get exposure to some of the best minds in the history of Comp Sci: the artificial intelligence field. Flaws will be found and corrected as usual. Used properly, though, LISP is dynamically and strongly typed: immune to vast majority of problems C/C++ languages experience without much effort on developer. Crashes in C/C++ are usually correctable exceptions in LISP that can be fixed while app is running. Its internal representation and evaluator has also been implemented in hardware before: risky native code was unnecessary. There’s also been security kernels and mathematically verified runtimes/compilers.

Despite designed opposite of security, LISP variants have actually achieved a lot more than C/C++ in that area with tiny funding. Quite impressive for a list processing language from 1956. It’s why I keep my eye on security-oriented papers for the event that someone finds better model for securing it. Absolute, sheer power plus security plus productivity plus good performance would be a dream come true. I’ll keep dreaming and waiting until these younger researchers in FP field invent it. They’re always inching closer.

@ Wael

“Some manifestations of the prison idea have been implemented before, although it would seem at a subconscious level, as an implementation of a security mitigation tactic.”

Sandboxing, “safe” interpreters, Google’s Python clouds… examples abound. Not bottom up, though: hacks to make unsafe code above work on unsafe platform below. Occasionally done bottom up: microkernels, type-safe OS’s, capability machines, crypto per page machines, etc.

“Some OS providers considered imprisoning developers by limiting a portion of device drivers to be implemented in “User Mode” — “Kernel Mode” device drivers would be no longer allowed. ”

POLA principle implied user-mode components. Typical microkernel approach. Even better models are lightweight formal verification (Microsoft) and synthesis from VHDL (NICTA). Btw, little known is that Microsoft from Vista onward changed drivers so they’d be mathematically verified to a degree. The verifier creates an abstract interpretation of the driver, models its interaction with Windows kernel API, and finds any risky interactions. Distributed free with Windows SDK. This is why we see so little driver failures and blue screens in modern Windows despite most running in the kernel. A little known and very successful use of higher assurance software methods by the last company you’d expect it to come from. 😉

“Going Top down is a different approach — a proactive one, where one uses the Prison construct as a Security Design Pattern. The Prison can have several manifestations, of which the above is just one possible understanding of many.”

You mostly just described POLA principle as it’s been used over the years while renaming it Prison. That’s some innovation. 😛

@ Thoth

“MingW32”

They’ll just hack your box and delete the original. You better have offsite backups for whatever you’re notarizing. 😛

@ All

This discussion reminds me of Paul’s excellent and enlightening essay about how UNIX turned into a pile of “festering hacks” nobody really understands. His claim was that modern developers raised in the bazaars wouldn’t know what a cathedral or good design looks like if they saw it. So, how could they be expected to build one esp working with bazaar’s offerings?

I think the concept applies to languages: some tools are better for building cathedrals than others. The tools inherent attributes map to inherent qualities of a cathedral. No surprise that much C/C++ code ends up in bazaars and horrendous proprietary software. The few counterexamples are produced by elite programmers.

Nick P • February 5, 2015 12:18 PM

@ Clive & people with heavy math background (esp proving)

Here is a brief tutorial and description of the sequent calculus that Shen uses as a type system. It’s a form of first order logic (eg PROLOG) with a certain structure and a bunch of inference rules. Unfortunately, it’s giving developers a hard enough time that they don’t use it. Like USL, it seems like they try to shoehorn everything into a rigid language to enable massive automation. Given difficulty of real proving, this might be justifiable if it is usable. Shen’s FP, macros, and LISP plus ability to use lightweight formal methods on any type or function indeed sounds powerful.

So, my question is what do you all think about Sequent Calculus combined with Shen? Shen author’s say most trouble comes from limited education people get in this kind of type theory and activity, even in math or formal methods classes. Maybe expressing it a certain way will get people on board and make it worthwhile. Or do you think it’s an inherently bad option and amateurs have a better route to full verification?

@ All interested in formal methods

An excellent textbook (free) for program verification with functional programming and Coq theorem prover. Throwing it in because most formal methods work uses Coq prover. Additionally, Adam Chlipala has a book on Certified Programming with Dependent Types. He’s used Dependent Types as a lightweight formal method to achieve many verification goals. So, that’s hitting it from another direction.

Nick P • February 5, 2015 5:12 PM

@ Grauhut

I’m aware of it. I’m talking about a scheme specifically for a company operating in the U.S. under U.S. law to avoid the backdoor issue similarly to Tor. While still making a profit or enough nonprofit revenue to support the offering. Far as Iceland, they’re one transoceanic cable cut away from losing data haven status or availability in event of an outage. Nobody else seems to notice that risk about them but it’s important given intelligence agencies messing with undersea fiber.

Hmm, on second thought, the Wassenaar Agreement affects most good countries for this sort of thing including Switzerland. Iceland’s crypto and press protections could be useful here. Same model as before except any encryption technology is developed and supported by an Icelandic foundation/company. They’ll have tools to integrate the crypto with the main software and the main software will be written to make such an integration easier. So, the crypto portion is just purchased and downloaded from Iceland with fewer restrictions given most democracies allow imports.

Nick P • February 6, 2015 12:46 PM

@ Gerard

We already discussed it here when you had a different name. I did look at more modern comparisons as you suggested.

@ Gerald, BoppingAround

I didn’t find much directly comparing Go against competitors except for this one. The author’s conclusions make it like Mozilla figured out how to make a lightweight, marketable Ada. It also protects memory operations without garbage collection. I’d take it over Go for low-defect systems programming.

@ Grauhut

I’ll be damned. My info was way out of date. Emerald Express is exciting as I’m pretty sure it’s that tech I posted on a few years ago where they used black magic to amplify existing fiber’s throughput up to terabit levels. Now we’re getting 40Tbit. Woo-hoo!

@ name.withheld

I would say “Cyanogen Mod coming to those very same smartphones near you!” Then, I see headlines where Microsoft is buying it out. (!) At least we still have the various encrypted chat apps to slow them down a bit.