On Thu, May 19, 2011 at 11:23 AM, Hans Georg Schaathun <h...@schaathun.net> wrote: > On Thu, 19 May 2011 10:23:47 -0700, geremy condra > <debat...@gmail.com> wrote: > : Let me get this straight: your argument is that operating *systems* > : aren't systems? > > You referred to the kernel and not the system. The complexities of > the two are hardly comparable.
I don't know about that. Among the many verified microkernels, at least two projects have formally verified both their kernel and their toolchain, and one of them claims they've verified everything in their TCB and are headed towards verified POSIX compliance in 2012. That would seem to be a fairly large system (and definitely a complete OS) to me. Another (seL4) says they've formally verified security of a complete system that includes a userspace and the ability to run other OSes in fully isolated containers, which also seems to be quite complete. Finally, there's one from Microsoft research that claims similar properties but which apparently isn't interested in compatibility, which I'm not sure how to interpret in terms of usefulness and size. In any event, higher level systems- like electronic voting mechanisms and automotive sensor networks- have also been verified, which seems to run counter to your original point. Also, not sure if it's open to the general public but if you're interested in this kind of thing and live near seattle, I think there's actually going to be a talk on verifying a POSIX userspace implementation here tomorrow. TL;DR version: large systems have indeed been verified for their security properties. > There probably are different uses of system; in computer security > literature¹ it often refers, not only to a product (hardware/software) > an actual installation and configuration of that product in a specific > context. /I/ did not redefine it. You chose a word with a many meanings, used it to make a very broad statement which is only a little bit true, and then pretended that you had the One True Definition in your pocket. I don't think that's legitimate, but whatever; let's just say that we meant different things by the word and drop it. > Speaking of reasonable assumptions, one necessary assumption which is > particularly dodgy is that whoever deploys and configures it > understands all the assumptions and do not break them through ignorance. Yup. Nothing is safe from idiots. > Is your concern with security purely from a developer's viewpoint, > so that you don't have to worry about the context in which it will > be deployed? My viewpoint is that of an attacker, since that's more or less my job. > I read your initial comment to imply that if you cannot get satisfactory > assurance using the lower levels, you won't get any at the higher > levels. That does not make any sense. Well, this is kind of like my point. My point was that you really don't get anything at the lower levels, and that they should fix that (which is far more useful to a normal consumer) rather than trying to talk about formal verification and similar tools, which are only going to be used on a tiny fraction of products. Geremy Condra -- http://mail.python.org/mailman/listinfo/python-list
