Log in

Quod Erat Dragon [entries|archive|friends|userinfo]
Quod Erat Dragon

[ website | Home page on the IETFNG public wiki ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Void type [May. 4th, 2015|04:21 am]
Quod Erat Dragon
A student / friend had asked for examples of Haskell's Data.Void's utility during office hours and I was drawing a blank so I gave some wimpy "Oh, Dependent Programming uses them to express things like complete matches using set differences" having completely forgotten its real power.  So I sent him:

While reading around the Internet today I was reminded of our conversation about Void and I, like a dunce, forgot an example that's vitally important: negation.  (There are some others, too, [0] that are less interesting.)

Types and logic have a lot in common; every well-typed program is a proof in a constructive logic corresponding to its type system.  The constructive form of the assertion "Not A" is actually "A implies Void", which has a natural type reading as an arrow type: a -> void (for a being the type corresponding to the proposition A).

That's all well and good, you're probably saying, but so what?  So think of the Continuation Passing Style transform:  every function of type a -> b becomes a function (a, b -> Void) -> Void, which we can read as "Not (A And Not B)" or "(Not A) Or (Not Not B)" or "A Implies (Not Not B)".  The CPS transform works because we can freely introduce double negation in a constructive logic!  In functional PL land, we can witness double negation introduction quite easily:

dni :: b -> ((b -> Void) -> Void)
dni b notb = notb b

Logically, this corresponds "Hey, you told me that both B and Not B were true!  Time to end the world."  "End the world" here, however, in CPS, is a clever slight of hand for "returning to the caller" -- it ends *the callee's* world, to be sure.

The reverse, incidentally, is not true!  Double-negation elimination's type would be "dne :: ((b -> Void) -> Void) -> b".  But that's pretty useless.  There's no way to conjure a function of type "b -> Void" to feed the argument and it wouldn't do us a whole lot of good even if we could.

However, there's a really amazing thing called "call with current continuation" in some languages, which has type (roughly; we can gloss over some details [2]) "callcc :: ((a -> Void) -> a) -> a".  What does this do?  Well, it takes a function "f" which *either* returns something of type a, in which case callcc returns that, or f invokes its argument with something of type a, in which case callcc returns *that*!  Can you see how to make dne from callcc?

More generally, callcc is essentially... the power to prove by negation!  Amazing... what?!  callcc says "If you can give me a proof strategy (function) which can take Not A and prove A, then I can prove A".  That is, if you provide a contradiction, callcc will provide the proof you wanted all along.

There's a story about a time travelling oracle here to tell, but perhaps it can wait.

[0] Broadly, any time you have a polymorphic function returning a something of a type variable that isn't mentioned anywhere else, you could instantiate it as Void and not alter the program's meaning or behavior (under assumptions [1]).  Why?  Because there's no way for the function to construct something type "forall a . a" (and given that the variable isn't mentioned anywhere else, we may as well shuffle the forall to the right of the arrow).

[1] Well, ahem, there are certain *rather alarming* exceptions, like the OCaml demarshaling library, which essentially has a function of type Representation -> String -> a.  In Haskell we'd probably use a GADT with phantom argument, "Representation a", but OCaml didn't have those.

[2] callcc is an alarming construct from the perspective of a language implementer who has efficiency on the mind!  It grabs the current (logical) stack frame and makes it a variable that's live in the program!  The program could do things like store it into data structures (to make a cooperative thread scheduler, even!  This is one of the assignments in CMU's second PL class)... or return it up the stack (oh *dear*) and invoke it later (resurrect finished worlds with fresh information; maybe it will go differently this time!)  There *are* ways of dealing with this, but they're somewhat slow (necessitating, essentially, copy-on-write stacks; never know if someone's about to re-invoke a past continuation... this construction is sometimes called a "cactus stack"); so usually one sees ST-monad-like type stunts for delimiting liveness of callcc continuations.
linktell me something

To all my friends who still read this [Nov. 27th, 2014|11:27 pm]
Quod Erat Dragon
I hope your Thanksgivings were wonderful, spent with family and/or friends and/or delicious food, as you desired.  Thank you all for being in my life.
link2 comments|tell me something

Faking multiple LDAP search bases with filters [Jun. 16th, 2014|01:42 am]
Quod Erat Dragon
So the ACM is setting up OpenStack and wanted to do something sort of odd: we want all our actual users to exist as users in OS's mind, but we don't want OS-specific users (e.g. "the" default OS administrative account) to exist as a real user.

Our LDAP database looks, in part, like:

  • dc=acm,dc=jhu,dc=edu

    • ou=People

    • ou=Users,ou=OpenStack

And it's conceivable that we'll have inetOrgPerson objectClass things elsewhere in the database that we don't want OpenStack to know about.  So really, we'd like multiple disjoint search bases: the ou=People one and the ou=Users one, but of course, we don't get that.  Their LCA is the dc=acm node, so we're going to run with that as our base.  We can, however, apply a filter that works just fine.  It's vaguely terrifying and in the worst syntax imaginable, but here it is:


What this says is basically that the objects returned must be (strict) subordinates to one of the two ou nodes I named above. You can, of course, use other match flavors and boolean logic and all that if you want.

The best part about this whole exercise, tho', is the complete and utter lack of documentation.  Despite readingI had to resort to fortunately finding mailing list posts http://www.openldap.org/lists/openldap-technical/201211/msg00116.html and http://www.openldap.org/lists/openldap-technical/201204/msg00223.html to actually understand how to do this.  The first hundred Google searches for what I thought would be plausible keywords didn't find anything.  Notice, further, that we can't do substring matches (the first thing I tried) on entrydn nodes, because they're not actually strings inside the database engine; they're references to DN objects.

Le sigh.  But here it is, maybe for another hapless LDAP user to find.
linktell me something

CM11 Trebuchet catapulted my phone into uselessness for an hour. [Jun. 12th, 2014|07:45 pm]
Quod Erat Dragon
Today's misadventure with software: CyanogenMod 11 Trebuchet (the app launcher; get it?) dies with "RuntimeException("Position exceeds the bound of this CellLayout")", rendering phone UI useless.

So I hook it up to my work machine and run adb shell and su. A little bit of selective modification of the database reveals that previous versions, which had suddenly stopped allowing more than 4 rows of icons, failed to purge the old rows from the database, but ignored them, and in the past 48 hours that seems to have gone from "ignore" to "crash uselessly the moment you see one". "delete from favorites where cellY = 4;" later I have a UI again and all my layout is still around, well except that this version seems to only allow me three panes; I guess I wasn't using that fourth one anyway!

I continue to hate software.

ETA: There's no in-UI way to work around this, either, other than the really brute force solution of deleting all of Trebuchet's data on the device and recreating one's layout by poking and dragging.  Gag me with a stick.
linktell me something

Software is terribad. [May. 29th, 2014|05:03 am]
Quod Erat Dragon
So today http://www.linuxsecurity.com/content/view/161587/ was brought to my attention.  I missed the patch when it went into tree months ago.  In any case, what, in general, do we do with tainted data that we 1) want to avoid interpreting and 2) are about to dump into a parser?  Well, we have some escape sequence in the parser's language.  Something that tells us that some chunk of text is just that: a chunk of text, or, if you insist, instead a single-character escape that you use whenever necessary.  This gets solved all over the place: TLV streams like ASN.1 (and protobufs and cap'n'proto and and and...) have this pretty easily, C and everybody inspired by C has its \ forms, XML has CDATA (and base64... let's not get into that too much), prose has indented blocks and quotation marks (and some handling for nesting them... OK, humans aren't perfect, but are not the target audience).  What don't we do?  Try to black-list "dangerous" strings that the parser might recognize.  Why?  Because it doesn't work!  People find ways around our blacklist, or the parser grows a new feature and our blacklist immediately becomes stale.

So, of course, when presented with a right answer and a wrong answer... we ended up here:

  1. xmonad grew a ppTitleSanitize hook (in XMonad.Hooks.DynamicLog) that, by default, tries to rip out known tags from xmobar (which means it's wrong as soon as xmobar adds another tag) and escape dzen strings (which is possibly fine; I haven't looked). Note that this is quadradic in performance.  Hooray. :(

  2. xmobar grew a "safe StdinReader" (as well as an Unsafe one) which regex-substitutes away action tags into less-harmful forms.  This is also wrong just as soon as somebody adds action2 or changes the grammar (again!  action tags have two forms) and it's really ugly, too.  Oh, goodie.

I just submitted a patch which instead of all of that BS simply adds to the parser the new form "<raw=LEN:STR/>", where LEN is the length of STR, which is the tainted data.  I need absolutely no post-processing anywhere in the stack, and my design still lets xmonad do things like make clickable desktop names ("feature" 2 above would strip those out in the default configuration; you have to deliberately switch to UnsafeStdinReader).

Maybe the "safe" stdin reader is a reasonable idea, separately from xmobar's use as a window manger component.  However, while the XMonadLog reader got similar treatment, the PipeReader, BufferedPipeReader, and CommandReader modules did not; there is no way (prior to my patch) to safely feed raw data in to xmobar on these channels.  A better fix is to eliminate the action parser from the parser stack altogether -- that is, pass the safety flag into the parser.

In any case, my patch is pending as https://github.com/jaor/xmobar/pull/168 ; if you build your own xmobar and want to play along, override your pretty printer's hooks to be something like this:

, ppTitle = HDL.xmobarColor "goldenrod" "" . xmoRaw . shorten 40
, ppTitleSanitize = id
-- ...
where xmoRaw x = "<raw=" ++ (show (length x)) ++ ":" ++ x ++ "/>"

The sole caveat to this encoding dance is that once you've encoded the raw string, you can't ever truncate it or you risk re-introducing injection attacks. (The output of ppExtras is appended to the string sent to xmobar, so a truncated encoded title is not guaranteed to be a parser failure.)

link1 comment|tell me something

Authenticated, encrypted, mirrored swap on FreeBSD 9 [May. 19th, 2014|11:59 pm]
Quod Erat Dragon
FreeBSD does not yet support swap on ZFS and probably will not any time soon (the ZFS memory lifecycle story is complicated and includes a lot of allocations at various stages). I took the opportunity of completely paving over my root filesystem (ahem: oopsies) to build a new setup. One of the minor annoyances of the old world was that the root and swap partitions had been installed on a single disk -- I never intended to make that my permanent home, it just sort of happened -- making a single disk failure catastrophic. And so! But here, we begin again. I'm now using ZFS in mirror arrangement across three disks for root, but that still leaves swap...

Read more...Collapse )
link1 comment|tell me something

UV-5R programming firmware bug workaround [May. 5th, 2014|12:12 am]
Quod Erat Dragon
I think I know several people with UV-5R radios. If yours, like mine, seem to crash every time you try to program them, don't give up; a little bit of brute force can, it seems, solve that problem. https://github.com/nwf/nwfsmallutils/blob/master/ham/uv5r.py will gladly read and write CHIRP-compatible radio images, even if the radio crashes mid-way through. If it's just me, I'll leave it as a standalone tool; if this issue affects others, I'll think about merging back into CHIRP itself.
linktell me something

Factotum heals a bleeding heart [Apr. 11th, 2014|02:03 am]
Quod Erat Dragon
[Tags|, , ]

So by now I'm sure everyone's heard about the heartbleed exploit in OpenSSL. If you haven't, please go read http://heartbleed.com now.

There have been a myriad of posts about the issue (e.g. Schneier's, HN, and many, many others), the code development practices of OpenSSL (e.g. Theo's commentary and the fascinating observation of an unfree() call) and some suggestions for dealing with the fallout long-term (Sean Doig's PGP-based proposal).

I would like to propose, in response to this and other issues with the current security software stack that we take a step back and rethink things. Rethinking the wire protocols is an excellent idea (I happen to think that QUIC's design is very nice) but there's something more fundamental in the current state of the world: almost all secrets are too public. Specific examples:

  • your web-server, a huge, complicated piece of code, has your private X.509 key

  • Unless you're using ssh-agent, every ssh process reads your keys. (Corrollary: every piece of software you run can read your keys.)

  • Every program you ever run has access to your Kerberos TGT, if you're using Kerberos, and will perform cryptographic operations with it, in its memory space.

What's the common thread? Big.complicated, network-facing codebases link against big, complicated, network-facing libraries and juggle your secrets in a way that you hope is secure. It probably isn't. This isn't the fault of the authors, per se; they're fighting an up-hill battle that's almost completely unwinnable, and have to win all the time; the adversary has to win just once. Even qmail has had a bug.

So what do we do?

We engage in process separation. We safeguard the secrets and restrict the set of operations that can be done with them to a safe set of operations that, notably, doesn't include "please reveal to me your secrets." We make the web servers, the firefoxes, the ssh servers, the ssh clients, everybody, mere men in the middle. Untrustworthy of handling every bit of power our secrets give us, just the power we think they need to have right now.

But wait, you say, I need those secrets to derive my session keys. I need them to prove that I am who I am. I need them to initialize the cryptographic protections. No. You need a black box into which you feed "I would like to X" and which eventually reveals "That worked; you have been connected to www.example.com with session key K." or "No, go away(, because Reasons)."

Before, we had clients and servers which spoke to each other and were carefully coded to not reveal the secrets they loaded and manipulated. Now, in this new future, we have clients and servers that couldn't reveal their secrets even if they wanted to: they don't know, and the black box won't tell them.

So how do we get here? Thankfully, some very smart people a long time ago invented a process called Factotum. Factotum is a separate process that speaks a very simple RPC protocol and does all your cryptograpy for you: see its manual page for details, but the basic idea is that clients and servers go through a phase where they simply shuttle messages between their associated factota and eventually factotum says yes or no. If yes, the clients and server start using the session keys the factota agreed upon.

Never again would we see a simple information disclosure exploit be so catastrophically bad as to reveal all our long-term identity secrets.

P.S. This idea appears to have been independently invented, specifically in the context of GSSAPI, as gss-proxy.

P.P.S. We could, if desired, move factotum (or gss-proxy) into the Linux kernel. Linux already has a notion of keyrings, and already has implementations of the cryptographic primitives we need, so we could dodge the additional context switches. That said, I am not sure it'd be worth it.
linktell me something

Church vs. Turing [Sep. 28th, 2013|01:07 am]
Quod Erat Dragon
[Tags|, , ]

My coworker Alex Rozenshteyn has just informed me that there's a much subtler relation between λ-calculus and Turing machines than I'd ever really realized. The Church-Turing result still holds, of course, but, as it was so eloquently put to me: "The devil's in the details." That is, the CT result says that the set of numbers computable by TM and λs are identical, but it says nothing about the "inner workings" of the processes, of either calculus, by which a number may be computed.

For the λ calculus, the sole "verb" is β reduction; in particular, this implies a meta-lemma that
∀ y . (λ x . x) y ≡αβη y,
which is hardly surprising, but... if I rephrase that a bit as
∀ C . C[ (λ x . x) y ] ≡αβη C[y],
we see immediately that the evaluation of this calculus cannot inspect its own syntax. (Well, cannot inspect and behave differently based on the result, at least.)

In the TM model, we know that there exist particular machines called Universal TMs, which are able to execute any other TM. That is, for any UTM U on tape symbol set Σ and any other TM M there exists a string m in Σ* such that U(m) and M are bisimulations; that is, if M on a blank tape terminates, U on a tape m terminates in the same way (i.e. by accepting or rejecting), and that if the latter terminates, so does the former. (There's a straightforward extension to starting on a non-blank tape, if that part worries you.)  But there's a really funny result for TMs: there's this lovely Recursion Theorem due to Klein which says (in one re-formulation) that for any UTM U and any TM M, there exists an equivalent TM M' which first writes the m from above to the blank tape and then behaves (in a bisumulative way, just as before) as M. Essentially, then, TMs always have access to their own syntax. This is the mechanism by which quines, autocannibals (and autocannibal-makers), "My SHA1 sum is: ..." and so on work.

But what about Church-Turing? That result implies the really awesomely subtle point: the ability to look at your own syntax must not actually matter. That is, there must be, for example, λ terms which reduce to (an encoding of) themselves in the SK calculus. In a bit more detail, there must exist at least one term Q which reduces to Q' = λ s k . Qbody such that the expression "Q' S K" (i.e., Q' (λ x y z . x z (y z)) (λ x y . x)) reduces again to (ETA: something equivalent to; thanks rntz!) Q'.  Functional quines, no syntax need apply! (If we reverse the arbitrary choice of order of S and K, then Q = K is an example; this is, to my mind, rather like the degenerate UNIX shell quine: an empty file.)

For the curious, there are extensions of the λ-calculus which do allow for syntactic introspection. Barry Jay invented the factorization calculus (alternatively, read the paper directly), a replacement for SK, which consists of S as before and a new F, with F being defined by pattern matching:
F O M N = M when the O parameter is S or F and otherwise, when O = P Q, F O M N = N P Q.
(I think I like theterm "Falcon" for F, since it is so good at pulling things apart; don't confuse it with the "Finch" combinator of other systems.) In such a system, we recover K = F F (or F S) the term F x K (K((SK)K)) returns a Church-encoded boolean indicating whether or not x is primitive. (The Finch or Viero combinators of course can be recovered as well and yield a combinator string which decides about its argument, if the use of x is unsettling.)
link5 comments|tell me something

OpenAFS rxkad rekeying on HEAD. [Sep. 20th, 2013|01:06 pm]
Quod Erat Dragon
Is anyone else here still running an openafs cell? :)

In any case, this is something of a PSA or at least a reminder to myself for when I do this again in a month: running HEAD is very different from running 1.6.5 as concerns rxkad. I'm sure this will change again as things merge, but for the moment, the instructions at http://www.openafs.org/pages/security/how-to-rekey.txt and http://www.openafs.org/pages/security/install-rxkad-k5-1.6.txt are not sufficient.

When generating a new key for your cell, you probably end up with a keytab which looks like this:
# ktutil -k /tmp/afsv5key list

Vno  Type                     Principal
  2  aes256-cts-hmac-sha1-96  afs/afs.ietfng.org@IETFNG.ORG
  2  des3-cbc-sha1            afs/afs.ietfng.org@IETFNG.ORG
  2  arcfour-hmac-md5         afs/afs.ietfng.org@IETFNG.ORG

As per the docs, if you have any des-* types in there, you've done something wrong or skipped a step. Apparently in some grand future (and in 1.6.5) the KeyFile will go away and you won't need to do anything other than land this keytab in the right place. Instead, right now, I had to run asetkey like this:
# for i in 16 18 23; do /usr/afs/bin/asetkey add rxkad_krb5 2 $i /tmp/afsv5key afs/afs.ietfng.org@IETFNG.ORG; done

where 2 is the Vno from above. Note that if you use 0 for the enctype in asetkey, it will run but produce a useless (buggy?) key file. Having done as above, restart the bosserver by hand and now you should be able to run bos restart localhost -all -localauth. If that complains, your keys are still in a bad state.

The numbers 16, 18, and 23 come from mapping the values in the "Type" column above via http://www.iana.org/assignments/kerberos-parameters/kerberos-parameters.xhtml#kerberos-parameters-1 (Though confusingly, 16, not 7. I don't know what the "-kd" means.)
link1 comment|tell me something

So I think I'll try this writing thing again [Sep. 6th, 2013|11:35 am]
Quod Erat Dragon
I've been thinking for a while that writing more often is likely a good idea, even if I don't have much to say. So you're all going to get some spam; I assume you know how to adjust things appropriately if you disapprove. :) So.

Today I gave my morning over to reading about the history of the ARPANET, again. While searching around, I found http://xn--brwolff-5wa.de/public/ , which included several documents I have not yet read and which seem to not be in the bitsavers archive (a mail has been dispatched). This reminded me that I do not know the fate of the IMP that went to CARNEGIE, so another email has been dispatched; I assume it went out as scrap a long time ago, but maybe it's just in some closet. (One hopes not in the flooded closet, but I did not see it there...) It really ought to be beside the C.mmp and cm* (which, incidentally, ought to be on public display!), but it's not.
link7 comments|tell me something

(no subject) [Mar. 31st, 2010|03:46 pm]
Quod Erat Dragon
re: http://www.lshift.net/blog/2010/03/31/what-has-happened-to-the-segment-registers

You know, we wouldn't need the OS to be involved if the LDT could be made to contain only ring-3 descriptors. One flag in the LDTR and we'd be done. Sigh.
link1 comment|tell me something

More reading material [Feb. 5th, 2010|11:48 pm]
Quod Erat Dragon

PL hackery:

http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf -- Kiselyov, Oleg and Shan, Chung-chieh. Functional Pearl: Implicit Configurations —or, Type Classes Reflect the Values of Types.

http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf -- Carette, Jacques and Kiselyov, Oleg and Shan, Chung-chieh. Finally Tagless, Partially Evaluated, Tagless Staged Interpreters for Simpler Typed Languages.

PL Theory:

http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf -- Pierce, Benjamin C. and Turner, David N. Local Type Inference.

http://www.cis.upenn.edu/~bcpierce/FOOL/papers9/shields.pdf -- Shields, Mark and Jones, Simon Peyton. First-Class Modules for Haskell

Formally verified compilers:

http://www.cl.cam.ac.uk/~mom22/jit/jit.pdf -- Myreen, Magnus O. Verified Just-In-Time Compiler on x86.

Logic programming:

http://www.cs.sunysb.edu/~tswift/webpapers/tplp-submit.pdf -- Swift, Terrance and Warren, David S. XSB: Extending Prolog with Tabled Logic Programming
link5 comments|tell me something

(no subject) [Jan. 1st, 2010|08:05 am]
Quod Erat Dragon
Happy New Gregorian Year, Livejournal.

My new year's resolution is 1280x800. What's yours?
link7 comments|tell me something

Root-causing the droid bug [Dec. 9th, 2009|06:27 am]
Quod Erat Dragon
I did some more digging in my checkout of the Android tree. You'll be

You will want to look at the Android tree's
( For contrast, see ./external/zlib/contrib/minizip/unzip.c )
and in particular this comment:

* Find the central directory and read the contents.
* The central directory can be followed by a variable-length comment
* field, so we have to scan through it backwards. The comment is at
* most 64K, plus we have 18 bytes for the end-of-central-dir stuff
* itself, plus apparently sometimes people throw random junk on the end
* just for the fun of it.
* This is all a little wobbly. If the wrong value ends up in the EOCD
* area, we're hosed. This appears to be the way that everbody handles
* it though, so we're in pretty good company if this fails.

And there's your 64K limit, kinda, sorta mostly.... The code looks for
101010256L == 0x06054B50 ("PK\x05\x06" little endian) which apparently
signals the End Of Central Directory. Anyway... That sequence occurs at
0x0a33ef3 (exploit) and 0x0a2756f (legit). The ZipFile.java code scans
forward from 64K back from the end of the file; the unzip.c code starts at
the end and walks backwards.

How about a magic trick?
I'm going to make this signature validity... disappear!
TA DA! It's ... gone!

Even more entertainingly, there is in fact some "junk" tossed on the end of
the file at this point, courtesy of Motorola and SignApk (it even tells us
so in the file)... the exploit zip doesn't begin until somewhere near
0x0a27c30 -- 1729 (or so) bytes of junk later, so there's your 63K limit for
this particular exploit.
linktell me something

un-zipping the droid's jar [Dec. 9th, 2009|12:27 am]
Quod Erat Dragon
[Tags|, ]
[Current Location |JHU]
[mood |geekygeeky]
[music |Covenant - Stalker]

I was pointed at a very curious file today. Since I can't rehost it here,
I'll just give the MD5 and SHA1 sum so you can google for it -- indeed google
has already indexed the MD5 sum to a few likely mirrors.

94a0c30ea9104c2776d042e760bfd716 droid-root.zip
20ad50644644097eb9914cdc18a2527503291d45 droid-root.zip

Anyway, how curious is this file? Well, it's this curious:

% mkdir unzip unjar
% (cd unzip; unzip ../droid-root.zip)
% (cd unjar; jar -xf ../droid-root.zip)
% diff -rq unjar unzip
Only in unjar: bp.img
Only in unjar: mbm.bin
Only in unjar/META-INF: CERT.RSA
Only in unjar/META-INF: CERT.SF
Files unjar/META-INF/com/google/android/updater-script and unzip/META-INF/com/google/android/updater-script differ
Only in unjar: patch
Only in unjar: rdl.bin
Only in unjar: recovery
Only in unjar/system: app
Only in unzip/system: bin
Only in unjar/system: fonts
Only in unjar/system: lib

Some additional fun facts about this file:
0000000 -- first byte of file, appears to be legitimate META-INF/MANIFEST.MF header & blob
0a22020 or so -- index of legitimate update.zip (META-INF/MANIFEST.MF entry)
0a27586 -- "signed by SignApk"
0a27600 and following -- appears to be HTC Certificate
0a27c3d -- start of next ZIP file? ("PK" and system/ entry)
0a27cc3 or so -- header & blob for /system/bin/su file
0a33970 or so -- index of illegitimate update.zip (META-INF/ entry)
0a3400e -- last byte of file

Observe the following (10648637 is 0x0a27c3d) :
% dd if=droid-root.zip of=test.zip skip=10648637 bs=1
50130+0 records in
50130+0 records out
50130 bytes (50 kB) copied, 0.163549 s, 307 kB/s
% file test.zip
test.zip: Zip archive data, at least v1.0 to extract
% mkdir unzip.sfx
% (cd unzip.sfx; unzip ../test.zip)
Archive: ../test.zip
error [../test.zip]: missing 10648637 bytes in zipfile
(attempting to process anyway)
creating: system/
creating: system/bin/
inflating: system/bin/su
creating: META-INF/
creating: META-INF/com/
creating: META-INF/com/google/
creating: META-INF/com/google/android/
inflating: META-INF/com/google/android/updater-script
error [../test.zip]: attempt to seek before beginning of zipfile
(please check that you have transferred or created the zipfile in the
appropriate BINARY mode and that you have compiled UnZip properly)

If you flip the dd around, the prefix is observed to be a perfectly sane .zip file,
handled by both unjar and unzip in identical ways.

So what we've got is a file which is secretly two zip files concatenated. The index
of the second is mangled so that some tool, namely unjar, blows by it in its search
for the index, but that another tool, namely unzip, does not.

And now for why this matters. Jar file signing is very clever: the list of files
and their hashes is generated and signed and the resulting signature detached and
itself stored in the jar. This allows multiple parties to attest to the contents
of the archive. However, what's happening here is that one tool -- the one verifying
the signature -- sees what it expects to see: the tail of the file (the second zip
file) is outside the archive and therefore doesn't alter the list of files inside
the archive or their contents. So the signature is still believed valid. The file
is then extracted again using a different tool which operates on the
second zip file. At this point, no signature or manifest checks are made, and
your phone is now correctly yours again.


P.S. The reason for the "error" message in the unzip command above is that the
second index has been told that there's this first zip file atop it and so it's
using "back-references" as a kind of compression to allow for more interesting
bits to fit in the exploitable window.
link1 comment|tell me something

(no subject) [Nov. 9th, 2009|05:23 am]
Quod Erat Dragon
[Current Location |OmegaComplex]
[music |VNV Nation - Savior]

Today, the weather was fantastic. I went hiking; in shorts and a t-shirt... in November. Hm. In any case...
First for 90 minutes next to campus wherein I got to listen to a naturalist explain some details about the local water shed and sewer system. Then, Blake happened and a small group of us piled into his car and did this: http://maps.google.com/maps/ms?ie=UTF8&hl=en&msa=0&msid=113225046552081406078.000477e8bbeeebcd91e2c&ll=39.410335,-76.836405&spn=0.018833,0.047722&t=h&z=15 . Had a Ramen and tea dinner there as well. Pretty good night sky... at least, much better than one sees in town.

Tomorrow, I give a presentation to the PL reading group about Complete and Decidable Type Inference for GADTs. The contrast entertains me.
linktell me something

410 [Nov. 2nd, 2009|02:49 am]
Quod Erat Dragon
[Current Location |OmegaComplex]

Between sully, jwise, and myself:

If you wish to terminate by corrupted heap, press 1.
For termination by concurrency, press 2.
If you would like to demonstrate your failure to understand 213, press 3.
For death by red-zoning, press 4.
For death by self-inflicted stack mangling, press 5.
To speak to a TA, please stay on the line.
If you do not wish to die, please drop the class.
link5 comments|tell me something

Rawr software [Oct. 29th, 2009|05:35 am]
Quod Erat Dragon
[Tags|, ]
[Current Location |OmegaComplex]
[music |The Alpha Conspiracy - Morphic]

I can't believe I spent three hours on this... http://www.freebsd.org/cgi/query-pr.cgi?pr=140073
linktell me something

There's gotta be a better way to do this, too... [Oct. 18th, 2009|06:18 am]
Quod Erat Dragon
[Current Location |OmegaComplex]
[mood |geekygeeky]
[music |Pendulum - In Silico - Propane Nightmares]

So I have a FreeBSD machine, named Hydra, that runs approximately a bazillion jails. Unfortunately, the network stack virtualization work isn't quite done yet, so I'm still in the era where jails are "just" addresses on the host's stack. First off, that's a fustercluck in its own right; the BSD model really falls to pieces here, but ignoring that...

I want jails and the unjailed world to have different access policies, and in fact the jails' should differ as well. In the BSD networking world, NAPT happens before filtering, which means that the filters see a clobbered view. To pass state through, it is necessary (?) to use a feature called "packet tagging". Thus, my /etc/pf.conf looks like this:
# macros bla bla bla
no nat on $if_ext from ($if_ext) to any tag ROOT
nat on $if_ext from $ip4_jail_csloungebot to !<rfc1918> tag JAIL_CSLOUNGEBOT -> ($if_ext)
nat on $if_ext from $ip4_jail_mrwright to !<rfc1918> tag JAIL_MRWRIGHT -> ($if_ext)
# ...

# Inbound shtuff
rdr pass inet proto tcp from any to ($if_ext) port 8888 -> $ip4_jail_csloungebot
rdr pass inet proto tcp from any to ($if_ext) port 31457 -> $ip4_jail_mrwright
# ...

block in all
block out all
block in quick from urpf-failed
pass out quick from ($if_ext) tagged ROOT
pass out quick inet proto tcp to any port 6667 tagged JAIL_CSLOUNGEBOT
pass out quick to ! <rfc1918> tagged JAIL_MRWRIGHT
# ...

the net effect is that things inbound trigger NAPT state and are just always permitted (the "pass" in "rdr pass"), but outbound things are more complicated: each jail's transmissions get NAPTed and shifted over to the right interface and tagged with its name and when it comes time to filter, the filtering rules key on tag. The real kicker is the "no nat" rule, which does "nothing" (it tags packets from the unjailed world) but must come first, since there it runs before the NAPT rules get to do their thing and mangle the view.

While here, it's worth mentioning that despite that jails have addresses all assigned on a (renamed) lo1, if you want to see packet flow, even to these addresses, you sometimes have to look on lo0 (perhaps only the case of actual loop-back; I amn't sure).
link2 comments|tell me something

[ viewing | most recent entries ]
[ go | earlier ]