[HN Gopher] TRRespass: Rowhammer against DDR4
___________________________________________________________________
TRRespass: Rowhammer against DDR4
Author : mdriley
Score : 54 points
Date : 2020-03-10 15:24 UTC (1 days ago)
(HTM) web link (www.vusec.net)
(TXT) w3m dump (www.vusec.net)
| kalium_xyz wrote:
| I wish we could get rid of this dependency on the natural world
| that computers seem to have. Sadly I cant of a way to implement
| computers outside of reality and have some safe interface to
| them.
| XorNot wrote:
| There's an SCP article somewhere in this...
| saagarjha wrote:
| Unfortunately, it looks like any interface is a potential for a
| side channel...
| heavenlyblue wrote:
| Is it? You can fix rowhammer by simply re-mapping all memory
| banks after executing every instruction.
| AnthonyMouse wrote:
| The dependency comes from pushing the physical limits until the
| abstraction leaks. Older memory technologies were not
| vulnerable to rowhammer. But they were also a lot slower.
| gentleman11 wrote:
| Theoretically, if we accepted lower performance, could we design
| our hardware and software to actually be secure? The number of
| exploits over the last two years is making my head spin
| danielheath wrote:
| You can (almost fully) solve this by using a rack of low-power
| computers, each running a single task, instead of a one faster
| one.
| Jap2-0 wrote:
| This brings up something I've often wondered about: we can
| basically guarantee that a very short snippet of code (say, a
| few lines) is secure, right? However, there is no real way to
| guarantee that full programs are secure. Can we not truly
| guarantee that some portion of code is secure, or is it simply
| the amount of code that makes it impractical (and financially
| infeasible)? If the latter, what is the practical boundary?
| Y-bar wrote:
| I think what you are asking for is Common Criteria.
|
| https://en.m.wikipedia.org/wiki/Common_Criteria
| saagarjha wrote:
| That seems to have the smell of incompetent bureaucracy...
| simcop2387 wrote:
| > we can basically guarantee that a very short snippet of
| code (say, a few lines) is secure, right?
|
| That's the problem, we can't do that. Between hardware flaws
| like rowhammer, meltdown, spectre, etc. it's not possible to
| say that a piece of code isn't going to trigger something
| intentionally or not.
|
| You can say that something very very likely doesn't trigger
| any known vulnerability, but only while also specifying the
| exact hardware to run it on and probably other external
| variables.
| Jap2-0 wrote:
| > Between hardware flaws like rowhammer, meltdown, spectre,
| etc. it's not possible to say that a piece of code isn't
| going to trigger something intentionally or not.
|
| I guess I was thinking software vulnerabilities
| specifically (although in the context of this article I
| should have thought about the hardware side more). Or to be
| even more specific, flaws that are from that program in
| particular.
| simcop2387 wrote:
| Software side there's a lot that can be proven and said
| about small sections of programs. I think a sibling
| commenter talked about an ISO standard related to that
| (And I think it covers some hardware bits). My layman's
| understanding of it is that it's a way to specify as many
| assumptions about how the code will be run, where, and
| what side effects it will have and no others. That makes
| for a really nice set of assertions but the end effect is
| that you can't say anything about certain kinds of
| programs; i.e. This program is safe, That program can't
| be safe, and then these programs are unknowable. Godel
| should never have been allowed to publish anything.
| sterlind wrote:
| You can formally prove that a program is a refinement of
| a specification, or that a subroutine always obeys
| certain invariants (when executed honestly.) See Dafny
| and ADA-SPARK for examples.
|
| It reduces to theorem proving with a SAT solver like Z3,
| if your language is Turing-complete and your invariants
| are abitrarily general. SAT solvers are fast and powerful
| these days, but the usual issues are:
|
| 1. It's too cumbersome to define invariants or write the
| type of specs that can check program correctness.
|
| 2. Things get exponential as state space increases.
|
| Modern checked languages are finally addressing #1,
| though they will sometimes have blind spots (e.g. Dafny
| can't reason about concurrency.)
|
| Writing programs as bundles of isolated, formally
| verified modules, then proving the correctness of the
| program with a high-level spec that assumes module
| correctness, lets you scale to real, large programs. This
| is how Dafny works, for example -- functions declare pre
| and post-conditions, and so Dafny can throw away its
| reasoning about callee function's internals when checking
| a caller.
|
| This strategy really is overlooked! It's powerful enough
| that you can eliminate memory/argument checks at compile
| time, ditch all your unit tests and _KNOW_ your program
| implements a spec. It should be mandatory for all safety-
| critical systems that can 't rely on hardware fail-safes
| (e.g. airplanes.)
|
| It just takes 3x as long.
| joosters wrote:
| _we can basically guarantee that a very short snippet of code
| (say, a few lines) is secure, right?_
|
| I'm not sure that's true, but even if it is, you have to ask:
| _Which_ few lines?
|
| Let's say we have the technology that can analyse (say) five
| lines of code and prove them completely correct and secure.
| That doesn't mean you can prove a 500 line program to be
| secure by running the analysis on each 100 sets of five
| consecutive lines. Code in one place can affect the logic
| elsewhere. So now to prove a 500 line program correct, we'd
| need to analyse every possible combination of 5 lines chosen
| from the 500 => 255244687600 different proofs to check!
| Jap2-0 wrote:
| I guess that forms the core of the issue, it's inherently
| exponential (or factorial?).
| AnthonyMouse wrote:
| It's not just that. Before you can prove anything
| "correct" you need to define what "correct" means. Now
| you have the meta problem of proving that your definition
| of "correct" is correct.
| saagarjha wrote:
| Turing complete.
| saagarjha wrote:
| In this case, you'd refresh more often.
| simcop2387 wrote:
| Or if you can spare the cost switch to SRAM instead. Not sure
| if the density would be comparable enough to be reasonable
| even with the 100x jump in price (source: pulled out of hat).
| wmf wrote:
| At scale the price and density would be correlated so it
| might be more like 10x.
| wyldfire wrote:
| might want to merge this with
| https://news.ycombinator.com/item?id=22547324
| cesarb wrote:
| IIRC, there was a proposal some time ago to use performance
| counters to detect a rowhammer attempt (high number of cache
| misses) and stop it (by pausing the offending process until the
| DRAM refresh can catch up). Did anything come out of it?
___________________________________________________________________
(page generated 2020-03-11 23:00 UTC)