Profile

Cover photo
Patrick Georgi
35,706 views
AboutPosts

Stream

Patrick Georgi

Shared publicly  - 
 
Some variety for +ron minnich 's collection. (supposedly in a grocery store)
The Internet's visual storytelling community. Explore, share, and discuss the best visual stories the Internet has to offer.
1
Add a comment...

Patrick Georgi

Shared publicly  - 
 
Those are some powerful automated proofs.
Probably not too fancy for scientists who work on such stuff for years, but I'm glad to see they're now stepping up to share that power with mere coders like me.
Home · About SPARK 2014 · Proof in Use · Resources · Contributors. Categories. Language · Formal Verification · Design Method · Certification · Open Source · Events · News · Papers and Slides · Videos · GNATprove Tips and Tricks: Bitwise Operations. by Clément Fumex in Formal Verification ...
4
Torsten Meißner's profile photo
 
It's also good to see, that you can use Spark with the embedded compiler targeting the ARM Cortex-M series. There was a nice talk about this @ FOSDEM.
Add a comment...

Patrick Georgi

Shared publicly  - 
9
Add a comment...

Patrick Georgi

Shared publicly  - 
 
Really a great slide :-) Even if the methodology is a bit ad hoc.

The formula they used is mentioned on the slide before (see http://de.slideshare.net/AdaCore/slides-his-2014secunethsr for the full deck): P(Defective Program) = P(Defective Line)^(SLOC)
2
Torsten Meißner's profile photo
 
I'm curious about how the performance of a system based on muen will be when it has to work with our new hardware module. Until now I have seen SW only systems.
Add a comment...

Patrick Georgi

Shared publicly  - 
 
That presentation looked boring at the beginning.

BIOS Write Enable, yawn A race condition, cute. And Intel even provides a bit to protect against that (why isn't that the default?!?).

But it got better when they started looking at UEFI boot scripts. They're written at boot time and give instructions what to do after a suspend/wakeup cycle to initialize the hardware again. So far, so good.

Where are those instructions? Turns out, in regular RAM. Every OS can overwrite them at will (because they're written at boot time, not at suspend-time), and the only reason they don't is that UEFI says "please leave this alone".

Which of course, the presenters didn't. And even a workaround, where that stuff is kept in SMRAM (outside the immediate control of the OS) didn't quite work because that secret data pointed back into regular memory.

And finally they figured out that non-volatile UEFI variables, which are stored in flash, are actually writable without sanity checks that way. Which allowed them to mess up even earlier code, getting around another protection mechanism.

And the final segue to the realization that once you control SMM, you own the flash (no matter what UEFI tries to do) raised a comment that Intel plans a hardware feature to lock that down. With a link to the patent for that feature.

Recap: Intel messed up. In hardware. In software. Several times. Their workarounds and protection measures don't quite protect the system until you're extra careful. And that's just this presentation.

There were similar incidents pretty much every year since 2009 (at least). One of them, found by Invisible Things Lab, was about Intel TXT, which is supposed to increase the platform's security - but because of a bug in their "Authenticated Code Module" used in that feature, actually lowered it by allowing trivial control over SMM to whoever looks at the box the right way.
And there is nothing someone outside Intel can do about it, because that code module is "authenticated" (read: signed), and so the broken code can't be fixed. It took them a while to release patched images, and I'm not sure if they even covered all platforms.

Now I looked at the patent's abstract. To quote: "writes are only allowed to the platform firmware storage location by an Authenticated Code Module"

If anyone has the legal capability to get Intel to cease&desist from ever writing or designing code again, please do so. It's a matter of IT security.
2
Patrick Georgi's profile photoMathias Krause's profile photo
3 comments
 
The "measuring mode" would be nice but the systems I've seen so far implemented an "immediate shutdown" policy. Toggling a single byte in the boot block -- even a byte not even executed -- made the system shutdown instantly on attempting to power it on. Only externally reflashing the chip with the vendor BIOS resurrected the machine. And, as the policy gets set by the manufacturer (see [1]), I guess there's not much one could do on such a system :(

[1] http://www.intel.com/content/dam/www/public/us/en/documents/datasheets/4th-gen-core-family-mobile-u-y-processor-lines-vol-1-datasheet.pdf, chapter 3.10

Gah, Prague! Not even a two hours drive... Too bad I missed it :/
Add a comment...

Patrick Georgi

Shared publicly  - 
 
I guess coreboot is entering the educational sector now
The best place to look is probably Coreboot. It's the boot firmware used by Google Chromebooks. (Github mirror links used here for politeness to the project's servers.) Taking Intel Haswell processors as an example (because I know this code path) we can sketch the general process.
6
Add a comment...

Patrick Georgi

Shared publicly  - 
 
Buchpreisbindung für E-Books. Dabei kann man die doch gar nicht kaufen, nur lizenzieren? kopfkratz
 ·  Translate
1
Add a comment...

Patrick Georgi

Shared publicly  - 
 
Interessantes coreboot Profil im Deutschlandfunk
 ·  Translate
Bei Computer-Software ohne Produkte von US-Firmen auszukommen ist schwer. Denn bevor freie Betriebssysteme greifen, macht im Normalfall eine nicht-quelloffene Software den Computer überhaupt erst betriebsbereit: das BIOS – aus den USA und damit ein mögliches Einfallstor für Spionage. Doch es gibt auch zu BIOS eine Alternative: Coreboot.
3
Add a comment...

Patrick Georgi

Shared publicly  - 
 
Let's see if that gets merged into gerrit (and released) in time for Google login using coreboot contributors to have a chance to migrate their accounts.
[plugin "gerrit-oauth-provider-google-oauth"] client-id = "" client-secret = "" link-to-existing-openid-accounts = true. * Preserve auth.type = OPENID in $gerrit_site/etc/gerrit.config. * Observe that LoginForm offers Google OAuth2 provider: [1]. * Sign in using this link ...
2
Add a comment...

Patrick Georgi

Shared publicly  - 
 
coreboot made it to mainstream tech media
 
An overview of Intel Boot Guard.
The UEFI firmware that boots up your PC is a closed, proprietary blob of code—and you can't change it out even if you wanted to. Here's why.
2 comments on original post
2
2
Adrian Marius Popa's profile photoMathias Krause's profile photo
Add a comment...

Patrick Georgi

Shared publicly  - 
 
Thanks to Linaro's tireless efforts to support UEFI and ACPI on ARM64, Windows 10 ARM64 binaries are seen in the wild now.
1
Add a comment...

Patrick Georgi

Shared publicly  - 
 
Now I know what makes me uncomfortable about the 'Linus isn't nice' debate - the assumption that community leaders need to do whatever necessary to make people comfortable. They don't. The other side of the coin is that people are free to go elsewhere.
3
Mathias Krause's profile photoPatrick Georgi's profile photo
2 comments
 
It's not a free pass in the sense that people will stay away from your project. If you're willing to live with that, sure, "do the Theo de Raadt" ;-)

Thing is, people seem way more concerned with trying to reform LKML than with building their own community where they can apply their rules. Since this approach to reform requires buy-in to a concept without seeing it in action, I'm not surprised about opposition.
Add a comment...
Story
Tagline
polymath in training
Work
Occupation
solving problems at the hardware/software boundary