Wow, this thing must have been fun to debug and maintain. And also, must be a challenge to optimize current generation CPUs for, with separate data and instruction caches... No wonder it never gained traction.
Yeah, I read somewhere that that was the reason everybody's given up on the Synthesis techniques today. A shame, in a way, as it was a really cool system.
As I understand it, though, the modern systems which replaced the Halon systems are (sometimes? always?) dangerous. In particular, the point of a CO2 dump is to physically force all oxygen out of the room very rapidly. I also read that a CO2 dump makes a loud disorienting shriek, which doesn't help if you're trying to figure out what's going on and get out of the machine room. I've never been in that situation, or even been trained for it.
Indeed! I found the Python C API fairly straightforward. But I've been quite impressed with what I've seen of Pyrex or Cython. The C API to Python involves a lot of verbosity and boilerplate code; Pyrex and Cython let you use Python-like syntax but be able to call C library functions directly. Pyrex and Cython translate to C, with all of the weird boilerplate code being auto-generated. So essentially you write it like Python and call it like Python and the C stuff happens magically in the background. Sounds lovely to me!
And, of course, the great upshot of this is that Python doesn't need to be as fast as Java or C# - the vast majority of code is not performance critical and when you *do* need to do an intensive calculation you can call into a C library (probably just using an existing one).
Soya3D (http://home.gna.org/oomadness/en/soya3d/index.html), for instance, is a 3D engine written in Python and Pyrex, which calls into a number of C libraries to do some of the heavy lifting. Developing 3D apps in Python using Soya's API is really very nice.
PySoy is a fork of Soya3d (http://www.pysoy.org/), I don't know what the balance of languages it now uses are.
Who said anything about "paying";-) I'm a grad student and currently out of funding, so nobody pays me anything.:-(
Back in the day my PhD supervisor's company used to pay me to do C coding on a consultancy basis - unfortunately I don't really have time for that these days, I want to finish writing up, then escape to the Real World of paying work. Still want to find a C coding job, though...
Doing C for systems-level stuff is quite nice - I think if I had to use C for ordinary programs I would enjoy it less well, I have perhaps been spoiled by the likes of Python.
My "real" work is in C, where it's very easy to get certain things done but very inconvenient to do most other things. My fun programming is in Python because it makes quickly knocking together something that works as straightforward as possible. The C stuff is fun too, actually - it's just not the kind of hacking I'd want to do in my leisure time. Spare time hacking is often done alone or collaborating with a small group of programmers; Python's structuring (or lack thereof, depending on your point of view) actually works quite well if there's just you working informally on the code. And the very rapid development and flexibility mean I can get a lot more functionality out for a given expenditure of leisure time.
Actually, though, my default in a professional environment would probably be Python if it was applicable and I was given the choice. I'd only use C if it's really necessary for the job.
Well, I'm not actually saying that they are planning to cash in / abuse their powers. I'm just noting that they're giving to their organisation powers which could be abused. Which is probably fine at the moment, if they consider themselves pure and uncorruptable for now. However, they're obviously worried about commercialisation. If, for instance, in 10 years time commerical interests have somehow taken control of their organisation and decide to exercise the rights they've been reserving on all the photos taken over that time period then that would be a problem and highly antithetical to the stated intent of this licensing deal.
It's a bit like the principle that you shouldn't vote in oppressive laws: it's not just a question of whether you trust the current administration to use them sensibly, it's also a question of whether less well-meaning successors could abuse them. I do generally think that a prerequisite to true freedom of expression is that it not be at somebody else's sufferance: if somebody is reserving the right to restrict what you say, this element of freedom is not there no matter how generous they are. In essence they're giving you a very very large reserve to live on but it's still them that sets your boundaries.
But the blog post stated privacy as a concern - I really intended to point out that that argument seems like a red herring. The example that you gave of a photographer on the book project is, I would consider, something of a case in point: the photographer was responsible, none of the individuals minded being in it so there is no privacy concern, yet publication is still not approved and cannot be published. I personally don't think it's reasonable for the organisation to do this, however it's their choice. I would, though, rather privacy not get trotted out every time somebody wants to restrict photography for other reasons.
Agreed that the lighting is usually not realistic in games - AIUI it's pretty computationally hard to do realistic lighting even if there is a will to do it.
I still think the unrealism described kinda is an uncanny valley effect though - in that Quake 3, for instance, looked sufficiently far from reality that you could kinda go "That's just a lo fidelity representation". The graphics were so (comparatively) basic that you didn't feel compelled to compare them with real life. With modern games, with the graphical quality being much higher in terms of resolution, polygon count, texture detail, etc it is now getting to the stage that it looks more like a slightly unreal photograph. The picture the OP linked is a good example - it looks like a digital photo of a scene that's somehow too perfect to be real.
Seems like "Privacy" is the new go-to excuse for people who want to make unreasonable / unusual demands about photographs. We care about our attendees' privacy so much that we want to own pictures of them! Even if we didn't take them, we want to own the pictures of them - for their own protection! It's for your own good, move along now. I'm seeing a vague and ironic similarity with the shopping malls who CCTV your every move but claim personal photography is forbidden to protect their customers' privacy. Sure, we want to own pictures of everyone - but you can trust us! Somewhat unlike the shopping malls, I can believe that this is probably true of the Burning Man organisers - they may very well be trying to protect their attendees and have no ill intent.
They may very well have good intentions. They want to restrict your freedom of expression but only in good ways! As creative people, though, if they want to prevent abuse of imagery from their event maybe they ought to have thought twice before giving themselves easily-abusable powers. Maybe they believe themselves pure enough and hard enough to corrupt from an organisational standpoint that this isn't a risk. They may also have a point in believing that a strength of the event is being somewhat "disconnected" from the usual freedom to take and display photographs. Maybe this is sufficient to justify these restrictions.
At the end of the day though, their attendees are creative people and should, hopefully, be able to just Burning Man by their actions - what their policy is *and* how they choose to enforce it. I don't think they're being entirely reasonable but then I won't be going anyhow;-)
By running device drivers in isolated virtual machines *and* using an IOMMU (for which you need suitable hardware, obviously) you can substantially reduce the harm device drivers can do... They won't be able to abuse DMA hardware to write to any memory locations they want, they're stuck with writing to memory that guests provide them with. If the guests do crypto / checksumming then that could in principle cut down device drivers' ability to do harm to a "mere" denial-of-service.
If you can do this then you could probably engineer a system with a relatively small trusted base. There's been an ongoing conversation about "dom0 disaggregation" under Xen, which I believe is aiming to do something like this - that would remove having an entirely Linux distro as part of the trusted computing base, which would be A Good Thing;-)
Although I'm discussing Xen, there's no reason that L4 or some other system could not use the same hardware to get the same effect. There have been various projects using L4 to isolate Linux or Linux drivers in VMs, so it's a logical thing for them to do too.
Re HURD - indeed, it would be nice if they had a release. The Mach version had things like userspace filesystems years before Linux has FUSE. Always struck me as a system with lots of benefits - and it would be nice to see the GNU project finally become a "complete" UNIX replacement. I was hopeful about their use of L4, as its known to be (capable of being) very fast. I'm really not sure where (if anywhere) they're going now; they do seem to lack a strong lead / direction, which like everything has both benefits and costs.
I didn't know NetBSD had Mach compatibility - do you mean it can run on top of Mach? That's cool. I don't, to be honest, know a whole lot about Mach - and to make things more complicated I have the impression there are several versions floating around out there. Minix is another OS that I've not become very familiar with.
DragonflyBSD is a very cool OS that I've been watching with enthusiasm for some time. I think it's a shame that they've not been able to complete their original SMP scalability work yet, as it was one of their original goals. But most of the other stuff they've been doing - HAMMERFS, SYSLINK, etc - are quite interesting. There's not been enough that's different about DragonflyBSD to get me running it just yet but that may change.
Btw, sorry if I repeated anything you already knew / had thought of.
Your original point was, I should say, highly valid in the sense that this isn't going to affect any of our desktop / server OSes very soon. But it's promising as an advance in the state of the art nonetheless. Also, I guess if they'd written "formally proven hypervisor", that sounds more useful and is also somewhat accurate - although I don't think anyone uses L4 commercially as a hypervisor. Another spanner any hypervisor will need some kind of device driver virtualisation which can often be a means of increasing the amount of trusted code (e.g. on Xen you basically trust all of the dom0 VM - including Linux - to do the right thing since it has IO privileges, even though the hypervisor itself is quite small).
The TUD:OS demo CD includes (IIRC) some sandboxed applications, such as some port of gpg to L4. It also features a minimal secure GUI that runs outside of Linux and can be used to isolate things - pretty cool.
GNU/Hurd always seems like a really awesome system to me. But last I read they had decided that L4 doesn't suit them and that they want to write a new microkernel. Disappointing:-( I really want to be able to use (and hack on) that thing but I'd like the project to look a little more well-defined first!
Disclaimer: my background is on working on Xen but I have a research interest in L4, amongst other things. Should also note that I've not yet RTFA'd but I will do as it sounds awesome.
Well, for one thing you can use L4 as a hypervisor. L4 doesn't provide much in the way of high-level functionality - but neither does hardware. It can act as a hypervisor for running Linux VMs on. Bang, you've just formally proven a hypervisor so you can - hopefully - make precise guarantees about security between VMs, etc. In reality the picture is unlikely to be quite so rosy, since you still need to provide virtual devices to your VMs and there are potential security holes in paravirtualised device drivers. Still, it's a step in the right direction - the direction being that we can be *really* certain about how isolated VMs are, despite sharing the same hardware. And that isolation is, after all, part of the core purpose of virtualisation.
Going a bit more futuristic / researchy, there's been various work on running special high-assurance applications directly on L4 *alongside* Linux. So, for instance, modified versions of your crypto apps can be protected from Linux kernel exploits by running them outside Linux on L4 and using a very narrow communications channel to minimise the available vectors for an attacker. Or, conversely, you could distributed untrusted "applet" code to people that can be run directly on L4 - then they can run it outside Linux so they don't have to trust it as much.
Some of these concepts are demonstrated on a (separate) L4-based demo OS here, which is pretty cool: http://demo.tudos.org/
Disclaimer: my background is on working on Xen but I have a research interest in L4, amongst other things. Should also note that I've not yet RTFA'd but I will do as it sounds awesome.
Paravirtualization is where you modify a kernel so that it can run on something other than "bare hardware". Often in this situation you call the kernel that *does* run on bare hardware the "hypervisor" to distinguish it from the Linux (or whatever) kernel running on top. In this case Linux is running on top of their L4 kernel as a userspace program - instead of accessing parts of the hardware to get its job done it uses L4 system calls. This is basically the same as what Xen does, with L4 taking the role of the hypervisor. Researchers working on L4 have been playing with Linux-on-L4 for many years - longer than Xen has been about, AFAIK.
One nice trick you get, in this case, is that you have the ability to run Linux programs on your nice, formally-proven microkernel. But alongside that you can still run programs *directly* on the L4 kernel, independently of Linux (or with some controlled interaction with it). So, say you have some untrusted code you want to sandbox - you can run it directly on L4, which (now) has proven security properties. Or perhaps you have a crypto app which you want to isolate from Linux in case a root exploit leaves it vulnerable - you can run it directly on L4, outside Linux. You could potentially do similar things for programs that need realtime guarantees - let normal applications get scheduled by Linux's scheduler and realtime apps run directly on L4.
Basically, having L4 there is giving you an ability to start other "virtual machines" running paravirtualised OSes or high assurance applications. It's always been part of the goal that because L4 is simpler than Linux you get to have high assurance that it'll do what it's supposed to. Now a derivative has been formally proven the guarantees could potentially be even better.
The TUD:OS demo CD website has some interesting information about a real-world system that mixes the ability to run (multiple) Linux virtual machines, plus isolated secure applications, all under a security-oriented GUI. It's a pretty cool demo and you can run it as a LiveCD: http://demo.tudos.org/
While our old paper ID cards were easily falsifiable, the new smart card is virtually impossible to falsify. It has a lot of physical security measures, a few holograms, engravings, etc. As to the chip, all the data in the chip is digitally signed by the government. The RSA private keys inside are generated by the card during personalisation, and are not extractable. I dare you try to create a false one. The British card seems to be a cheap piece of shit.
By etching the surface off a chip and probing, smartcard forgers can do a surprising amount of snooping on a smartcard. There are countermeasures you can take against this, of course, so it's all a matter of who has the most resources. The British card being a cheap piece of work would not surprise me in the least.
Anyway, what's all the fuss about ID cards? What do you use to identify yourself? Social Security card? Driver's license? How hard it is to forge one of these?
Our current government, at least, seems to have some kind of compulsion to build databases on everything. It's not clear to me that they always know what their motivations are, they just seem to think that holding more information about their citizenry is always a good thing. Not a healthy attitude for a government to have, in my (and many others) opinion, so that's one objection. Another objection is the incredibly frequent leaks of government data - both classified intelligence-related stuff and their databases of citizens details. Often these are caused by people who should know better doing really stupid stuff like leaving disks on the train, in bars, etc.
Finally, there's the fact that nobody seems to really be able to articulate convincingly why we need ID cards. You have them in Portugal, they're part of your system, maybe they work well for you. Other European countries have them too. But in the UK we have systems for identifying ourselves "well enough" to any authority that needs to know who we are, without requiring a centralised point of data collection. The governments vague statements about stopping terrorism / benefit fraud / conservative fear of the month are not convincing, partly because they seem to be trying various "it's just to stop bad people!" explanations and seeing which stick, which doesn't exactly suggest sincerity. And partly because their reasoning seems somewhat flawed: if the people carrying out terror attacks are legally in the UK (as has happened in our recent past) then how much use would the ID cards be for stopping them; if the cards are implicitly trusted as unforgeable, the motivation to create knock-off cards to facilitate benefit fraud is greatly increased.
In essence the fuss is because our government has demonstrated they can't be trusted to even implement such a scheme competently, let alone use it only for the good of its citizens, and they have failed to demonstrate that they even know what they're trying to achieve. Given we already have processes in place for identifying ourselves without them, the insistent "we'll introduce them whether or not anyone notices, by the back door if necessary" way the government is pushing them seems to be cause for concern.
Horrible for many, useful for others - it depends on price and on what you need it for. I'd use it whilst away from my desk at home and whilst traveling. Most people wouldn't want one but there could still be enough to be a market.
I would not want it enough to pay through the nose for it (a la OQO) - but if they had netbookish pricing they'd have my attention. Basically the same hardware, so seems possible. My own netbook has such a small keyboard that I'd want to bring an external keyboard anyhow - and if I have to do that, no point having a laptop-style keyboard making the device bigger. x86 is a manky architecture but it is also cheap and popular; having it available gets me the full slew of desktop OSes for my "netpad".
What's likely to happen, I fear, is that we'll get some horrible combination of what I want and what you recommend - an x86-ish smartphone running some weird OS. I don't know if that'll be awesome or terrifying.
The user could still buy the Apple dev kit if they wanted to "legitimately" install their own version. Obviously that's very expensive and requires a Mac, so it's not ideal.
Really, though, although there's no GPL violation this is very much like the "Tivo-ization" everyone worries about. The Tivo runs a Linux kernel but is locked down to make it harder to install your own, modified Linux kernel.
Any hardware platform that is set up to restrict software installation / modification to be under the control of the device manufacturer, not the user, is vulnerable to this sort of "GPL paradox". It sucks. As a consumer, it's the kind of thing I like to avoid, but to some people (including myself) getting a "black box" I can't modify is OK in some domains. Not on my desktop, not my netbook, not my media box. I put up with it for my Xbox. But I wouldn't put up with an iPhone, simply because there are functionally similar and more open alternatives.
... if it were cheap enough. Seriously. OQOs, despite all their limitations and faults, were *awesome* if you wanted what they had to offer. I don't think they had entirely the wrong idea with their product, they were just a) ahead of their time and b) too expensive.
I met a chap at Linux Kongress in Hamburg who was running Linux on his OQO (the original one). He was able to demonstrate his x86 Linux development project on it. It was capable of VGA output, so he was able to run his presentation from it too. And it was small enough to fit in a (large-ish) pocket. The promise of a palmtop fulfilled, in a way. It doesn't matter that it's underpowered - so are netbooks and those are plenty popular.
A netbook-based OQO-like device would totally rock. I'm sure modern technology is up to the task of putting together a *cheap* device in an OQO-alike form-factor. If one were available at a reasonable price (i.e. a bit cheaper or about the same price as a netbook) I'd be very interested in picking one up. Media player, internet browser, ebook reader, running full desktop software. Plug in a keyboard and screen if you need to do anything serious on it - the market also should be capable of producing a docking station with laptop screen + keyboard with a DVI cable on, so that you can carry it around in a laptop case to supplement your palmtop device if you anticipate doing more serious browsing or typing.
The closest things to this that I currently see in development are the OpenPandora (http://openpandora.org), which isn't PC compatible but is pocketable and has a mini keyboard, clamshell design, runs Linux. And the new Intel MID chipset, which may not (?) be PC-compatible from what I've heard but will be x86-based and therefore able to run normal PC software for any OS that can boot on it in the first place. These should give us some of what we want - but hopefully some enterprising company will see the potential for a true netbook-based OQO-alike.
Slashdot Mirror
This tech sounds awesome in an evil way. Or evil in an awesome way, I guess.
I used capitals and punctuation correctly! I am no barbarian ;-)
Tpying ahs runed my ablty.
Wow, this thing must have been fun to debug and maintain. And also, must be a challenge to optimize current generation CPUs for, with separate data and instruction caches... No wonder it never gained traction.
Yeah, I read somewhere that that was the reason everybody's given up on the Synthesis techniques today. A shame, in a way, as it was a really cool system.
As I understand it, though, the modern systems which replaced the Halon systems are (sometimes? always?) dangerous. In particular, the point of a CO2 dump is to physically force all oxygen out of the room very rapidly. I also read that a CO2 dump makes a loud disorienting shriek, which doesn't help if you're trying to figure out what's going on and get out of the machine room. I've never been in that situation, or even been trained for it.
Indeed! I found the Python C API fairly straightforward. But I've been quite impressed with what I've seen of Pyrex or Cython. The C API to Python involves a lot of verbosity and boilerplate code; Pyrex and Cython let you use Python-like syntax but be able to call C library functions directly. Pyrex and Cython translate to C, with all of the weird boilerplate code being auto-generated. So essentially you write it like Python and call it like Python and the C stuff happens magically in the background. Sounds lovely to me!
And, of course, the great upshot of this is that Python doesn't need to be as fast as Java or C# - the vast majority of code is not performance critical and when you *do* need to do an intensive calculation you can call into a C library (probably just using an existing one).
Soya3D (http://home.gna.org/oomadness/en/soya3d/index.html), for instance, is a 3D engine written in Python and Pyrex, which calls into a number of C libraries to do some of the heavy lifting. Developing 3D apps in Python using Soya's API is really very nice.
PySoy is a fork of Soya3d (http://www.pysoy.org/), I don't know what the balance of languages it now uses are.
Anyhow, awesome stuff, sorry for rambling.
Who said anything about "paying" ;-) I'm a grad student and currently out of funding, so nobody pays me anything. :-(
Back in the day my PhD supervisor's company used to pay me to do C coding on a consultancy basis - unfortunately I don't really have time for that these days, I want to finish writing up, then escape to the Real World of paying work. Still want to find a C coding job, though ...
Doing C for systems-level stuff is quite nice - I think if I had to use C for ordinary programs I would enjoy it less well, I have perhaps been spoiled by the likes of Python.
My "real" work is in C, where it's very easy to get certain things done but very inconvenient to do most other things. My fun programming is in Python because it makes quickly knocking together something that works as straightforward as possible. The C stuff is fun too, actually - it's just not the kind of hacking I'd want to do in my leisure time. Spare time hacking is often done alone or collaborating with a small group of programmers; Python's structuring (or lack thereof, depending on your point of view) actually works quite well if there's just you working informally on the code. And the very rapid development and flexibility mean I can get a lot more functionality out for a given expenditure of leisure time.
Actually, though, my default in a professional environment would probably be Python if it was applicable and I was given the choice. I'd only use C if it's really necessary for the job.
Well, I'm not actually saying that they are planning to cash in / abuse their powers. I'm just noting that they're giving to their organisation powers which could be abused. Which is probably fine at the moment, if they consider themselves pure and uncorruptable for now. However, they're obviously worried about commercialisation. If, for instance, in 10 years time commerical interests have somehow taken control of their organisation and decide to exercise the rights they've been reserving on all the photos taken over that time period then that would be a problem and highly antithetical to the stated intent of this licensing deal.
It's a bit like the principle that you shouldn't vote in oppressive laws: it's not just a question of whether you trust the current administration to use them sensibly, it's also a question of whether less well-meaning successors could abuse them. I do generally think that a prerequisite to true freedom of expression is that it not be at somebody else's sufferance: if somebody is reserving the right to restrict what you say, this element of freedom is not there no matter how generous they are. In essence they're giving you a very very large reserve to live on but it's still them that sets your boundaries.
But the blog post stated privacy as a concern - I really intended to point out that that argument seems like a red herring. The example that you gave of a photographer on the book project is, I would consider, something of a case in point: the photographer was responsible, none of the individuals minded being in it so there is no privacy concern, yet publication is still not approved and cannot be published. I personally don't think it's reasonable for the organisation to do this, however it's their choice. I would, though, rather privacy not get trotted out every time somebody wants to restrict photography for other reasons.
Agreed that the lighting is usually not realistic in games - AIUI it's pretty computationally hard to do realistic lighting even if there is a will to do it.
I still think the unrealism described kinda is an uncanny valley effect though - in that Quake 3, for instance, looked sufficiently far from reality that you could kinda go "That's just a lo fidelity representation". The graphics were so (comparatively) basic that you didn't feel compelled to compare them with real life. With modern games, with the graphical quality being much higher in terms of resolution, polygon count, texture detail, etc it is now getting to the stage that it looks more like a slightly unreal photograph. The picture the OP linked is a good example - it looks like a digital photo of a scene that's somehow too perfect to be real.
Seems like "Privacy" is the new go-to excuse for people who want to make unreasonable / unusual demands about photographs. We care about our attendees' privacy so much that we want to own pictures of them! Even if we didn't take them, we want to own the pictures of them - for their own protection! It's for your own good, move along now. I'm seeing a vague and ironic similarity with the shopping malls who CCTV your every move but claim personal photography is forbidden to protect their customers' privacy. Sure, we want to own pictures of everyone - but you can trust us! Somewhat unlike the shopping malls, I can believe that this is probably true of the Burning Man organisers - they may very well be trying to protect their attendees and have no ill intent.
They may very well have good intentions. They want to restrict your freedom of expression but only in good ways! As creative people, though, if they want to prevent abuse of imagery from their event maybe they ought to have thought twice before giving themselves easily-abusable powers. Maybe they believe themselves pure enough and hard enough to corrupt from an organisational standpoint that this isn't a risk. They may also have a point in believing that a strength of the event is being somewhat "disconnected" from the usual freedom to take and display photographs. Maybe this is sufficient to justify these restrictions.
At the end of the day though, their attendees are creative people and should, hopefully, be able to just Burning Man by their actions - what their policy is *and* how they choose to enforce it. I don't think they're being entirely reasonable but then I won't be going anyhow ;-)
... I have the power to control time - bedtime!
You made an awesome reference. You don't deserve to be languishing down here at +2. Still, you made me happy!
The Amiga Hand was the boot screen, not an error screen.
But ... but ... you can't wear a boot on your hand!
By running device drivers in isolated virtual machines *and* using an IOMMU (for which you need suitable hardware, obviously) you can substantially reduce the harm device drivers can do ... They won't be able to abuse DMA hardware to write to any memory locations they want, they're stuck with writing to memory that guests provide them with. If the guests do crypto / checksumming then that could in principle cut down device drivers' ability to do harm to a "mere" denial-of-service.
If you can do this then you could probably engineer a system with a relatively small trusted base. There's been an ongoing conversation about "dom0 disaggregation" under Xen, which I believe is aiming to do something like this - that would remove having an entirely Linux distro as part of the trusted computing base, which would be A Good Thing ;-)
Although I'm discussing Xen, there's no reason that L4 or some other system could not use the same hardware to get the same effect. There have been various projects using L4 to isolate Linux or Linux drivers in VMs, so it's a logical thing for them to do too.
Re HURD - indeed, it would be nice if they had a release. The Mach version had things like userspace filesystems years before Linux has FUSE. Always struck me as a system with lots of benefits - and it would be nice to see the GNU project finally become a "complete" UNIX replacement. I was hopeful about their use of L4, as its known to be (capable of being) very fast. I'm really not sure where (if anywhere) they're going now; they do seem to lack a strong lead / direction, which like everything has both benefits and costs.
I didn't know NetBSD had Mach compatibility - do you mean it can run on top of Mach? That's cool. I don't, to be honest, know a whole lot about Mach - and to make things more complicated I have the impression there are several versions floating around out there. Minix is another OS that I've not become very familiar with.
DragonflyBSD is a very cool OS that I've been watching with enthusiasm for some time. I think it's a shame that they've not been able to complete their original SMP scalability work yet, as it was one of their original goals. But most of the other stuff they've been doing - HAMMERFS, SYSLINK, etc - are quite interesting. There's not been enough that's different about DragonflyBSD to get me running it just yet but that may change.
Btw, sorry if I repeated anything you already knew / had thought of.
Your original point was, I should say, highly valid in the sense that this isn't going to affect any of our desktop / server OSes very soon. But it's promising as an advance in the state of the art nonetheless. Also, I guess if they'd written "formally proven hypervisor", that sounds more useful and is also somewhat accurate - although I don't think anyone uses L4 commercially as a hypervisor. Another spanner any hypervisor will need some kind of device driver virtualisation which can often be a means of increasing the amount of trusted code (e.g. on Xen you basically trust all of the dom0 VM - including Linux - to do the right thing since it has IO privileges, even though the hypervisor itself is quite small).
The TUD:OS demo CD includes (IIRC) some sandboxed applications, such as some port of gpg to L4. It also features a minimal secure GUI that runs outside of Linux and can be used to isolate things - pretty cool.
GNU/Hurd always seems like a really awesome system to me. But last I read they had decided that L4 doesn't suit them and that they want to write a new microkernel. Disappointing :-( I really want to be able to use (and hack on) that thing but I'd like the project to look a little more well-defined first!
Disclaimer: my background is on working on Xen but I have a research interest in L4, amongst other things. Should also note that I've not yet RTFA'd but I will do as it sounds awesome.
Well, for one thing you can use L4 as a hypervisor. L4 doesn't provide much in the way of high-level functionality - but neither does hardware. It can act as a hypervisor for running Linux VMs on. Bang, you've just formally proven a hypervisor so you can - hopefully - make precise guarantees about security between VMs, etc. In reality the picture is unlikely to be quite so rosy, since you still need to provide virtual devices to your VMs and there are potential security holes in paravirtualised device drivers. Still, it's a step in the right direction - the direction being that we can be *really* certain about how isolated VMs are, despite sharing the same hardware. And that isolation is, after all, part of the core purpose of virtualisation.
Going a bit more futuristic / researchy, there's been various work on running special high-assurance applications directly on L4 *alongside* Linux. So, for instance, modified versions of your crypto apps can be protected from Linux kernel exploits by running them outside Linux on L4 and using a very narrow communications channel to minimise the available vectors for an attacker. Or, conversely, you could distributed untrusted "applet" code to people that can be run directly on L4 - then they can run it outside Linux so they don't have to trust it as much.
Some of these concepts are demonstrated on a (separate) L4-based demo OS here, which is pretty cool: http://demo.tudos.org/
Disclaimer: my background is on working on Xen but I have a research interest in L4, amongst other things. Should also note that I've not yet RTFA'd but I will do as it sounds awesome.
Paravirtualization is where you modify a kernel so that it can run on something other than "bare hardware". Often in this situation you call the kernel that *does* run on bare hardware the "hypervisor" to distinguish it from the Linux (or whatever) kernel running on top. In this case Linux is running on top of their L4 kernel as a userspace program - instead of accessing parts of the hardware to get its job done it uses L4 system calls. This is basically the same as what Xen does, with L4 taking the role of the hypervisor. Researchers working on L4 have been playing with Linux-on-L4 for many years - longer than Xen has been about, AFAIK.
One nice trick you get, in this case, is that you have the ability to run Linux programs on your nice, formally-proven microkernel. But alongside that you can still run programs *directly* on the L4 kernel, independently of Linux (or with some controlled interaction with it). So, say you have some untrusted code you want to sandbox - you can run it directly on L4, which (now) has proven security properties. Or perhaps you have a crypto app which you want to isolate from Linux in case a root exploit leaves it vulnerable - you can run it directly on L4, outside Linux. You could potentially do similar things for programs that need realtime guarantees - let normal applications get scheduled by Linux's scheduler and realtime apps run directly on L4.
Basically, having L4 there is giving you an ability to start other "virtual machines" running paravirtualised OSes or high assurance applications. It's always been part of the goal that because L4 is simpler than Linux you get to have high assurance that it'll do what it's supposed to. Now a derivative has been formally proven the guarantees could potentially be even better.
The TUD:OS demo CD website has some interesting information about a real-world system that mixes the ability to run (multiple) Linux virtual machines, plus isolated secure applications, all under a security-oriented GUI. It's a pretty cool demo and you can run it as a LiveCD: http://demo.tudos.org/
While our old paper ID cards were easily falsifiable, the new smart card is virtually impossible to falsify. It has a lot of physical security measures, a few holograms, engravings, etc. As to the chip, all the data in the chip is digitally signed by the government. The RSA private keys inside are generated by the card during personalisation, and are not extractable. I dare you try to create a false one. The British card seems to be a cheap piece of shit.
By etching the surface off a chip and probing, smartcard forgers can do a surprising amount of snooping on a smartcard. There are countermeasures you can take against this, of course, so it's all a matter of who has the most resources. The British card being a cheap piece of work would not surprise me in the least.
Anyway, what's all the fuss about ID cards? What do you use to identify yourself? Social Security card? Driver's license? How hard it is to forge one of these?
Our current government, at least, seems to have some kind of compulsion to build databases on everything. It's not clear to me that they always know what their motivations are, they just seem to think that holding more information about their citizenry is always a good thing. Not a healthy attitude for a government to have, in my (and many others) opinion, so that's one objection. Another objection is the incredibly frequent leaks of government data - both classified intelligence-related stuff and their databases of citizens details. Often these are caused by people who should know better doing really stupid stuff like leaving disks on the train, in bars, etc.
Finally, there's the fact that nobody seems to really be able to articulate convincingly why we need ID cards. You have them in Portugal, they're part of your system, maybe they work well for you. Other European countries have them too. But in the UK we have systems for identifying ourselves "well enough" to any authority that needs to know who we are, without requiring a centralised point of data collection. The governments vague statements about stopping terrorism / benefit fraud / conservative fear of the month are not convincing, partly because they seem to be trying various "it's just to stop bad people!" explanations and seeing which stick, which doesn't exactly suggest sincerity. And partly because their reasoning seems somewhat flawed: if the people carrying out terror attacks are legally in the UK (as has happened in our recent past) then how much use would the ID cards be for stopping them; if the cards are implicitly trusted as unforgeable, the motivation to create knock-off cards to facilitate benefit fraud is greatly increased.
In essence the fuss is because our government has demonstrated they can't be trusted to even implement such a scheme competently, let alone use it only for the good of its citizens, and they have failed to demonstrate that they even know what they're trying to achieve. Given we already have processes in place for identifying ourselves without them, the insistent "we'll introduce them whether or not anyone notices, by the back door if necessary" way the government is pushing them seems to be cause for concern.
I'm not that into Pokemon.
When I see a printout copy of XKCD I have this urge to hover my finger over the surface of the page, waiting for a bonus punchline to appear.
It's a really weird feeling.
Horrible for many, useful for others - it depends on price and on what you need it for. I'd use it whilst away from my desk at home and whilst traveling. Most people wouldn't want one but there could still be enough to be a market.
I would not want it enough to pay through the nose for it (a la OQO) - but if they had netbookish pricing they'd have my attention. Basically the same hardware, so seems possible. My own netbook has such a small keyboard that I'd want to bring an external keyboard anyhow - and if I have to do that, no point having a laptop-style keyboard making the device bigger. x86 is a manky architecture but it is also cheap and popular; having it available gets me the full slew of desktop OSes for my "netpad".
What's likely to happen, I fear, is that we'll get some horrible combination of what I want and what you recommend - an x86-ish smartphone running some weird OS. I don't know if that'll be awesome or terrifying.
The user could still buy the Apple dev kit if they wanted to "legitimately" install their own version. Obviously that's very expensive and requires a Mac, so it's not ideal.
Really, though, although there's no GPL violation this is very much like the "Tivo-ization" everyone worries about. The Tivo runs a Linux kernel but is locked down to make it harder to install your own, modified Linux kernel.
Any hardware platform that is set up to restrict software installation / modification to be under the control of the device manufacturer, not the user, is vulnerable to this sort of "GPL paradox". It sucks. As a consumer, it's the kind of thing I like to avoid, but to some people (including myself) getting a "black box" I can't modify is OK in some domains. Not on my desktop, not my netbook, not my media box. I put up with it for my Xbox. But I wouldn't put up with an iPhone, simply because there are functionally similar and more open alternatives.
... if it were cheap enough. Seriously. OQOs, despite all their limitations and faults, were *awesome* if you wanted what they had to offer. I don't think they had entirely the wrong idea with their product, they were just a) ahead of their time and b) too expensive.
I met a chap at Linux Kongress in Hamburg who was running Linux on his OQO (the original one). He was able to demonstrate his x86 Linux development project on it. It was capable of VGA output, so he was able to run his presentation from it too. And it was small enough to fit in a (large-ish) pocket. The promise of a palmtop fulfilled, in a way. It doesn't matter that it's underpowered - so are netbooks and those are plenty popular.
A netbook-based OQO-like device would totally rock. I'm sure modern technology is up to the task of putting together a *cheap* device in an OQO-alike form-factor. If one were available at a reasonable price (i.e. a bit cheaper or about the same price as a netbook) I'd be very interested in picking one up. Media player, internet browser, ebook reader, running full desktop software. Plug in a keyboard and screen if you need to do anything serious on it - the market also should be capable of producing a docking station with laptop screen + keyboard with a DVI cable on, so that you can carry it around in a laptop case to supplement your palmtop device if you anticipate doing more serious browsing or typing.
The closest things to this that I currently see in development are the OpenPandora (http://openpandora.org), which isn't PC compatible but is pocketable and has a mini keyboard, clamshell design, runs Linux. And the new Intel MID chipset, which may not (?) be PC-compatible from what I've heard but will be x86-based and therefore able to run normal PC software for any OS that can boot on it in the first place. These should give us some of what we want - but hopefully some enterprising company will see the potential for a true netbook-based OQO-alike.
http://dilbert.com/strips/comic/2008-06-20/