electronvolt

Yeah, I bike regularly on and off (season/mood/goals dependent, honestly), and knowing what I should expect on my commute to work /and/ back is important... and not something I can predict without looking at the weather in the morning.

I guess I'd say -- I think you're right that you shouldn't (ideally) be able to trigger true deadlocks/livelocks with just serializable transactions + an OLTP DBMS.

That doesn't mean it won't happen, of course. The people who write databases are just programmers, too. And you can certainly imagine a situation where you get two (or more) "ad-hoc" transactions that can't necessarily progress when serializable but can with read committed (ad-hoc in the sense of the paper here: https://cacm.acm.org/research-highlights/technical-perspecti...).

I mean, you say that, but systems like Spanner exist & I think the fact that it's used for Gmail, Docs, etc. has demonstrated that for a large range of OLTP workloads, serializable everywhere and also performant /is/ possible to architect for -- with the right combination of both database + application design.

That isn't to say it's correct everywhere, but I'd maybe be a little more suspicious of "We want OLTP but we can't use serializable" in a vacuum.

Of course--there are obvious cases like "We can't use serializable because of how our database implements it" or even "because we can't be arsed to figure out how to structure all our data accesses to avoid conflicts and aren't paid enough to solve that problem", but I feel like those are a bit more honest than "Because of performance reasons, in all cases". :)

You can, with some programming languages, require a proof of this (see: Rocq, formerly 'coq').

I think a more interesting case might be showing functional equivalence on some subset of all inputs (because tbh, showing functional equivalence on all inputs often requires "doing certain things the slow way").

An even more interesting case might be "inputs of up to a particular complexity in execution" (which is... very hard to calculate, but likely would mean combining ~code coverage & ~path coverage).

Of course, doing all of that w/o creating security issues (esp. with native code) is an even further out pipe dream.

I'd settle for something much simpler, like "we can automatically vectorize certain loop patterns for particular hardware if we know the hardware we're targeting" from a compiler. That's already hard enough to be basically a pipe dream.

I mean, in C++ (17? 20? Whenever constexpr was introduced) it's totally possible to create a library that allows you to build a SQL query via the language's string concatenation libraries/etc., but only allows you to do it with static strings unless you use ~shenanigans. (C++ unfortunately always allows ~shenanigans...)

I guess you do wind up needing to potentially re-implement some basic things (or I guess more complex, if you want format string support too). But for basic string concatenation & interpolation, it's reasonable.

That's a pretty useful way to get basic string concatenation while also preventing it from creating opportunities for SQL injection.

For example, you have a class that requires a constexpr input & can be appended to/concatenated/etc.:

SqlStringPart(constexpr ...)

operator+(SqlStringPart ...)

(so on)

And you have a Query API that only takes SQL string expressions that are built out of compile time constants + parameters:

SqlQuery(SqlStringPart ..., Parameters ...);

This doesn't solve the problem mentioned in the article around pagination & memory usage, but at least it avoids letting someone run arbitrary SQL on your database.

Proofs are actually incredibly hard to review. Problems will be found in what had been accepted to be a "good" proof years to decades later. There's a whole movement to move proofs over to something/anything more verifiable (e.g. representing all proofs in Coq--but even then you're relying on the Coq proof assistant to have zero bugs).

Furthermore, the standard for mathematical proof has also changed over time, most significantly in the early 20th century. This led to a number of existing results needing to be re-proved (or thrown out! Some were incorrect!).

Exactly what qualifies as a proof is a FASCINATING debate. Mathematics is created by consensus, just like all other knowledge.

Yeah, all I was really saying was that the grandparent's comment and the parent's comment weren't in opposition.

Microsoft owns the data center the code lives in and certainly takes care of physical security.

I disagree. Phone encryption should ideally be open source-able and it's security should rely as entirely on a device specific key as possible.

I think this makes more sense for a secret project (e.x. the next iPhone), but honestly as a security person it seems overkill for anything outside national security responsible code, like state sponsored malware.

I also find it strange that the code is apparently somehow accessible outside that building (see the fired comment). If this was anything beyond security theatre, it'd be on an airgapped network and that wouldn't even be a concern (as the employee wouldn't be able to access the code from their laptop). Seems excessive for very little gain.

Yeah, which is hosted on Azure, a data center that Microsoft owns and employs guards for, and secured behind our standard corporate authentication. :) (Source: I work at Microsoft, near the VSTS team.)

It's definitely true that Meltdown is a more immediate problem--but Spectre is basically the problem that will last. We can move kernel memory into another process space, take the perf hit, and correct most of the meltdown problems.

Spectre style issues had JS pulling browser process memory using timing--the patches being "put every page in its own process" (Chrome) and "don't let people get accurate timings" (Firefox). They are way worse in the grand scheme of things, because even if they aren't as easy to exploit, they will continue to show up, probably for the foreseeable future (next 5-10 years), long after Meltdown is patched and old news.

I'd disagree as far as your position on the word "gender"--I think actually "race" is a much better example of something that has had many meanings over the course of its lifetime in the language, and isn't necessarily well defined even now.

Gender as a term that relates to people, and not words (as in the sense of the gender of a noun in Latin-family languages), has been pretty well defined since it was introduced in the 1950s--specifically as a way to differentiate between biological sex (male, female, intersex, etc.) and the social roles that people play that may or may not actually be related to biological sex (men/women/boy/girl/etc.). It's always been quite well defined, although some people feel that it either doesn't make sense to differentiate between biological sex and gender (e.x. because, perhaps, they believe that social gender roles are innate conditions of biological sex).

But, the whole of his complaint rests on this deficiency. It's not possible to constructively disagree with someone who is unwilling to acknowledge basic facts, or who promotes an alternate reality.

This really needs to be emphasized--if you cannot agree on what the facts are, you will never come to a real conclusion. This is something the article completely glosses over. However, I also I think there's also something beneath just agreeing on what constitutes facts that is equally important, which is a (roughly) shared value system.

The old, "liberally educated" world that the author references the death of in the 1960s (i.e. "Closing of the American Mind") was one of shared values--largely white, protestant values. What replaced it was a different value system--I've seen it called the "meritocratic" value system, or similar--which had fundamentally different core values, and was/is dominant among American conservatives and liberals until recently.

Currently, the furthest left and furthest right often don't agree on core values. On the left, I think almost any argument that uses a variation on "(holy text) said so" can be dismissed off-hand as an unconvincing argument when you're talking about things beyond your own personal behavior--however, my Mormon relatives feel quite differently. This gets uglier and further away from the mainstream when you start to dig into some of the belief systems that groups on the alt-right propose (simplifying, but often things like "only white people have intrinsic value"), as opposed to the mainstream belief systems of the last ~40 years ("all people have intrinsic value"). Similarly on the far left, I've seen a lot of disagreement with other things that I'd hold up as mainstream values of the last 40 years (such as "competition between independent actors leads to good outcomes for consumers*").

Disagreements when fundamental values differ will put any argument on hold before it gets started, and I expect the only real outcome is things that devolve into shouting matches, or worse. And from what I've seen, the range of acceptable values has widened dramatically in the last 15 years--I'm curious to see if this winds up coalescing into a new set of mainstream values after a while, or if things like the structure of the internet/"filter bubbles"/increased ideological splits will mark the end of an ideological "mainstream" as it used to exist.

Late response, but: coq has the optional verification that you're proposing. :)

In my experience, Coq is not significantly harder than OCaml to write unverified code in. It's missing some nice shorthand syntax, but other than that it feels pretty similar.

With coq, the main challenge is expressing things that are meant to "run forever" (any truly unbounded recursion)--but my understanding is that would be forced to halt when it ran out of ether (so it's bounded anyways, and if you needed to you could probably explicitly hand that fact to the compiler)--and I think you probably don't want something to loop indefinitely if each iteration costs ether.

The main issues with coq that I think you'd crop up against are things that a good optimizer/compiler could probably help with (e.x. things like the fact that integers are naively represented as cons cells, so addition is O(n) and multiplication is worse). However, I haven't written any smart contracts, so it's definitely possible I'm missing something obvious.

I'd agree, and the article basically says the same thing--the language is too expressive, and therefore hard to analyze. I don't know that much about the Ether devs, but I'd expect it just didn't occur to them--even among PL folks, knowledge & experience with something like coq is somewhat rare unless you went to the right undergrad or grad school. Especially if you weren't keeping up with the latest research in the last ~5-10 years or so.

Something like Coq with a few primitives to represent interacting with the Ether network, and an optimizing, verified cross compiler would have been a perfect fit for this sort of thing, in my opinion. It's a shame that they didn't go that route, the extra dev time to get it right probably wouldn't have been equivalent to 200+ dev-years of cost (~31 million).

We're not even close to a world where tools can offer amazing protection.

Actually, we're reasonably close--the tools aren't quite there yet for mass consumption (many are still feel quite researchy), but given that the trend of (research -> industry) usually takes 10-25 years, I'd expect that more and more critical systems will be formally verified in 10 years. Even now, companies like Amazon are using some formal methods (modelling with TLA+) to validate that specifications will behave as expected. (https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-...)

Formal methods & dependent types allow for some very cool tricks on top of that--basically, you can encode in the type system a proof that the program implementation matches a specification. CompCert is a mostly-formally verified C compiler--since it was released, iirc, no bugs have been found in the verified portion of the compiler. (CompCert page: http://compcert.inria.fr/man/manual001.html)

You can also prove that the specification has particular properties (in a distributed system, things like liveness and partition tolerance). Consider the Verdi framework (allows formal verification of distributed protocols) and their formal verification of RAFT. (Code here: https://github.com/uwplse/verdi-raft)

However--it's just that it currently takes a lot more work in terms of person-hours to do the development. But formal methods are getting used in more and more places, and they do make a difference in practice. (Wired has a not particularly deep, but straightforward article that shows another use: https://www.wired.com/2016/09/computer-scientists-close-perf... )

Anecdotally, as far as effort--I'm an industry programmer who writes mostly C#. I had to learn Coq (a formally verified language) for a class--it took me a couple of simple assignments to get the idea of how it worked. Even after a few months, hacking together a formally verified interpreter for a very simple language (functions, while loops, etc.--simple, but not trivial) took about 3-4 times longer than it would have taken me to do normally.

So it turns out you can basically use type theory to encode a surprisingly large number of desirable traits about your program. (Caveat being that as you get more restrictive, you reject more "good" programs at compile time--no free lunch with Rice's theorem.)

For example: In this paper, they basically use types (with an inference algorithm) to catch kernel/user pointer confusion in the Linux kernel. (https://www.usenix.org/legacy/event/sec04/tech/johnson.html)

It turns out you can encode a lot of other interesting properties in a type system (esp. if you're building on top of the existing type system), though--you can ensure that a java program has no null-dereference checks (https://checkerframework.org/ has a system that does this), and Coq uses its type system to ensure that every program halts (as a consequence, though, it isn't actually Turing complete).

There's also cool things like Lackwit (http://ieeexplore.ieee.org/document/610284/) which basically (ab)used type inference algorithms to answer questions about a program ("does this pointer ever alias?", etc.).

I'll have to watch this later, but I'd argue the issue, at least for me, isn't really surface level understanding. (At least, the kind I think could plausibly be imparted in 4 minutes. :))

The basic idea of deep learning has always seemed straightforward to me[0]. However, at least my perception is that it feels like there's a lot of deep magic going on in the details at the level that Google/Microsoft/Amazon/researchers are doing deep learning. That's honestly true of most active research areas[1], but since those results are also the results that keep getting a lot of attention, the "it's a black box" feeling makes sense to me. :)

[0] Having done both some moderately high level math and having a CS background, I feel like most ideas in CS fit this description, though. Our devil is the details.

[1] For instance: fairly recent results in weird applications of type theory are also super cool, and require some serious wizardry, but those get much less attention. (And are, I think, more taken for granted, since who doesn't understand a type system? /s)

I'm getting kind of sick of this "deep learning is a black box" trope, because it's really not true anymore.

That's fair/probably true.

I think there's two things that drive that--one, lack of a widely shared deep understanding of the field[0] (and not really needing a deep understanding to get good results--as both you and the author pointed out), and two, the fact that it feels like cheating, compared to the old ways of doing things. :P

[0] When the advice on getting a basic understanding is "read a textbook, then read the last 5 years of papers so that you aren't hopelessly behind", there just isn't going to be widespread understanding.

I think you're kind of missing the author's point.

My feeling is that the "perfect" abstraction of reality to geometry is actually a very high order function that we don't fully understand.

You don't need a perfect abstraction of reality, though. All you need to do is get close enough to catch up with humans or outperform them and you've solved most of the hard problems in computer vision. Fortunately--at human scales, which are the only ones you need to care about for computer vision, reality behaves closely enough to a pure Euclidean space that you're fine. :)

The author's primary argument seems slightly more nuanced, too, than just "It'd be nice if we could use old techniques".

Basically, they're claiming that if you can build geometric understanding into the ML model, you will get significantly better results that just naively plugging and chugging away with raw data. That's an empirical claim that can be validated by researchers--either it will give a significantly improved performance on well defined problems (stereo vision, etc.) or it won't. Vision is one of the research areas that have developed pretty good benchmarks over the years. :)

You get other advantages for doing three/five node replication--online updates are free if you require (n-1) compatibility.

Reality is that if you need to hit 5+ nines and require strong consistency guarantees (like "we never lose our customer's data") at data center scale, you'll probably need something similar. Most people probably don't need those guarantees, however.

Having experienced slight feelings of melange/detachment following novels, video games, and movies in the past, and having experienced what this article is describing: it's not quite the same feeling.

With movies/novels/etc., I've always experienced what you're describing as something similar to a feeling of loss--the world you experienced or the story you were involved in or the characters you cared about will no longer be there as a new experience, no longer have new experiences as characters, etc. That 'world' is gone.

With VR, even if I don't really miss the experience, I've experienced what I'd describe as a "readjustment" phase of between 10 minutes and a couple hours (depending on length of experience and how recently I'd been in VR) where the real world feels disconnected/less real. It's a much more intense and visceral feeling, and doesn't have the same undertone of 'loss' that movies/novels have. It isn't a "Man, I'm not actually a space pilot in the year 3000" feeling, or a "I'll never be able to experience that world again" feeling, it's more of a visceral disassociation from the real world, as though my senses don't feel like they can quite trust the inputs they're receiving anymore.

"If it ain't broke, don't fix it." goes for attacks, too.

Why spend weeks/months searching for 0-days and hoping they will remain viable when you can spin up a fake login page and a bit.ly, find the people to target and send the targeted emails in a couple of days, max?

here are at last 3 obvious approaches: (1) applying the functions sequentially, (2) concatenating their outputs, (3) XORing their outputs. None of these takes rocket science to figure out, and some 5 seconds of thinking would easily rule out #1 and #2 as inferior to #3.

This is wrong. Concatenation would be harder to attack than XOR. Finding two things which hash to to two particular values in two separate hash functions is necessarily harder than finding two things which will hash to values which will XOR to the same value--almost a priori. You replace a double collision (across two hashes) which is very unlikely with an XOR collision, which is going to be exponentially easier.

You're simultaneously literally claiming that two secure ciphers can be combined to result in an insecure cipher when their keys are generated independently. This is far more astonishing than the claim that the ciphers you're using are actually secure in the first place.

Since you seem to want practical examples on recent crypto: consider meet in the middle attacks on 2DES as an example of why combined cryptosystems are not necessarily as strong as you'd imagine. It's admittedly a weak example--still stronger than 1DES, and an old system. Fundamentally, combining cryptosystems, even with separate keys, gives you a new cryptosystem which requires separate analysis.

Hell, you haven't even shown shown this is possible for any pair of secure ciphers; your "example" was missing the most crucial part of the cipher -- the key. The whole argument is so crazy it's just utterly ridiculous.

If I had a good attack on RSA + ECC, I'd be writing a paper about it. I'm gonna posit that if that's the kind of proof you want to believe you're "wrong", you'll remain happily "correct" in this scenario.

I don't know when you read my comment, but I edited it (I think) some ~15 minutes before you posted your comment to clarify that I wasn't referring to stacking arbitrary hashes. Read it again. I was referring to stacking hashes that are already thought to be cryptographically secure.

It still doesn't make a difference in my argument. My point is that you gain no added strength via a stacked hash implementation because it's as weak as the first hash in the sequence, and that it is potentially worse because you can also attack it via attacks on later hashes in the sequence.

A stacked hash is as weak as the first hash in the sequence--this should be obvious. A collision in the first hash function will obviously cascade into all later ones, so your stacked hash function is as weak, or strong, as the first hash function. That means you gain no strength.

What I was showing via an obvious/contrived example (to keep the math easy) was that it is also possible to attack a stacked hash via weaknesses in later hashes in the sequence. I wasn't (I thought obviously) implying that you'd intentionally choose a hash that was weak for a middle one--but there are all sorts of hashes we once thought were secure that we don't think are secure anymore.

I feel like you should already realize this (in which case I don't get why you're posting the comment), but while that's a cute mathematical existence proof, it's totally irrelevant as it's not something that can just happen out of the blue.

Fundamentally, all modern crypto relies heavily on math. I made a "cute mathematical existence proof" to make it obvious how stacking ciphers can weaken an encryption system. The reality is that exactly how ciphers interact is a subtle and hard to measure point, but it isn't safe to assume that composing cryptosystems will be as secure as either cryptosystem on its own, because features of the two systems could interact to weaken the overall security of the cryptosystem.

Two layers is at least as secure as a single one of either layer.

This is not uniformly true for cryptosystems--it is not naively the case that P(Q(X)) is a secure form of encryption, just because P/Q is. A contrived example is when P and Q are inverses (so P(Q(X)) is plaintext), but it should be obvious that if P has the wrong interaction with Q it might make some of the message easier to attack.

The question is whether it will hurt, and the answer is that it does not. Again, this is common sense.

It can hurt. It's subtle, but consider if a hash in the middle has a distribution issue (extreme case--hash in the middle maps everything to 0, now your entire hash stack is broken). In short: stacked hashes are no stronger than the first hash in the sequence (collision there = collision in the stacked algorithm) and have the potential to be weaker.

I'd argue that they pretty clearly are different, if you're talking about generic laziness-as-a-quality versus subject specific laziness.

Someone who isn't interested in school might be willing to work very hard at improving in a sport, or work very hard on their extracurricular club, or work very hard to teach themselves assembly and programming, or to learn a musical instrument. They might even be willing to work hard to teach themselves math, but be uninterested in putting effort into math class.

I guess it depends on if you consider "laziness" a universal character quality or not.

Which can (and should) be stored in a way that requires a password to access (ssh supports this, as do most other certificate systems).

1. From glancing at it: this is a pretty ugly solution.

On the plus side: It's minimal and doesn't spend much time building abstractions on top of the basic lists/etc. that scheme provides. However, it certainly isn't pretty.

For instance: Things like the king & knight checks are really pretty ugly brute force solutions.

Similarly, the variable & function naming really is rather unclear and very poorly commented--some of that may be use of things idiomatic to scheme that I'm unfamiliar with though.

2. Always a possibility, I certainly don't know you. ;)

3. Some people certainly have said that before and probably will again. This is really just a personal preference thing, I think.

(Note: I work for Microsoft, although not on the OS. I mostly use Debian and Ubuntu at home for things other than gaming, and know a bit about security--but I'm a bit rusty since I wasn't following it from 2010-2014 and haven't really thought about how to attack things since 2008-2009. These are my opinions/thoughts and don't represent the company I work for at all.)

Windows has been harder to attack than OS X since Vista. I don't think that's changed--Apple is generally slow to correctly implement security features that require kernel changes compared to either the Linux devs or Microsoft.

If I remember correctly, OSX didn't have a good ASLR implementation until 10.9 or 10.10, and has generally lagged behind on OS-level security updates and exploit mitigation (NX pages, ASLR, etc.). It was routinely the first thing hit in the early Pwn2Own competitions (partly because exploits on it were a breeze, partly because the laptop was usually a little nicer and you only got the laptop back then, too--but also because moving from crash to reliable exploit was easier).

I haven't followed security updates in Linux in the past few years as closely, so I can't comment on it as knowledgeably. From what I remember, it was about on par with Windows for difficulty to attack in Vista/7, but there's been a lot of security features that Windows has added since then. From what I remember, a fully hardened Linux box was just as bad to attack as a hardened Windows box, but Windows has generally required less configuration to get that right. (I think SELinux still isn't enabled by default in some distros?)

I think the fundamental thing is that it is not a rational fear--nuclear is associated with bombs that flatten cities and radiation is, to many people, a simply scary unknown that they can't touch, smell, or see, but which might kill them. (Many of the people I've met who were against nuclear power didn't really emotionally understand radiation as something you get some of every day anyways--it's a bogeyman that gives you either cancer or superpowers.)

Smoke/smog, in comparison, is something you can see and can expect to interact with daily if you're in a city. Despite the fact that it's much more dangerous, people don't perceive it as such.