Slashdot Mirror

It's not so useless, Mr. Cafe. Case in point:

Bitcoin attack: https://eprint.iacr.org/2014/1...

GnuPG attack: http://www.nicta.com.au/pub-do...

ASLR attack: http://www.internetsociety.org...

All of these are cache-based side-channel attacks.

It is possible to mathematically vertifiy code (see l4, its expensive and time consuming. But for something like this it would make sense to do it once and do it right.

The important observation is that the halting problem applies to software in general. If you take some subset of software, like, say, the set of programs that will pass a competent code review, then you probably will be able to solve the halting problem for those pieces of software. When proving complete formal correctness of a program (something which is not done often because with current techniques it takes absurd amounts of time from people with very specialized knowledge), you often intentionally design the program along with the proof so it is easier to make the proof go through. The papers on the design of the seL4 proven correct microkernel are a very interesting view into this process.

(Also, the halting problem is way harder than NP, it's recursively enumerable, which is sorta like NP in that elements of the set can by verified by a program except unlike NP which requires the program run efficiently (polynomial-time), recursively enumerable has no time limit, which is why you can't use that program to prove a negative: you can't distinguish waiting for the program to finish eventually from a program that will actually never finish.)

Now, prove the formal correctness of Linux.

What bothers me is that Microsoft has really good engineers but lacks a clear strategic direction. Their massive amount of legacy code plus some seriously bad "assumptions" about what the users want have sustained their decline in the last 10 years. It's a sad state of affairs, having used their products since Windows 1.0 when they were "the rebels".

I know it's just my opinion, but given their deep pockets, they should create an incubator unit or a completely separate start-up with huge funding for a re-acquisition later on (similar to what Cisco is doing with Insieme). The purpose of this group should be to go back to their roots, and re-think the way people and companies are expected to interact with computers in the next 10-20 years timeframe, and create a brand new OS with no legacy code, and anticipating the challenges and threats that will evolve overtime as much as possible.

I've always wondered why airplanes and MRI machines can have "mission critical" OSs and software while we all have to deal with crashes and uncertainty. They have the capability to create and bring to market a practical, usable EAL-7 OS. We know it has been done before, but Microsoft has the capability to make it commercially viable for everyone. And this is only ONE of the things they could do.

I think the article and DHS are a few years behind the curve on this. See these guys:

http://www.nicta.com.au/media/previous_releases3/2012_media_releases/australian_face_recognition_technology_wins_major_international_ict_award

Also, there are a couple of live systems out there that I've heard about in airports. They could add facial recognition, but mainly they're used for object detection.

Javascript is Turing-complete, so validation would require infinite time.

This is false.

Properties of Turing-complete languages can be verified in finite time. The catch is that to do so, you must reject some valid programs. For example, think about a typed programming language like Java: if you take a correct program and change a type annotation to "Object", the program is still "correct" in some sense, but will fail to compile. In that sense, the type-annotations constitute a kind of proof to the compiler that the code is type-correct and therefore satisfies certain safety properties (e.g. all method calls are on objects that support that method or on a null reference, which, in compiled code, may be equivalent to not treating some user data value as a function pointer which could allow arbitrary code execution).

There is absolutely no reason why a Javascript implementation cannot be made safe (in the sense of not executing arbitrary code; you can't prevent it from crashing because, as you said, it's Turing-complete so it might have infinite loops). For example, the Quark research project builds upon WebKit but uses more sandboxing than modern browsers to give much stronger guarantees about what websites can and can't do. Of course, that relies on the OS kernel's sandbox being correct, but those are much, much simpler than Javascript sandboxes, so that is a pretty safe (and even possibly formally verifiable) assumption.

First, you misstate Goedel's Incompleteness Theorem: it says either those trees don't cover the whole space or they overlap, not both (although both is certainly possible). That's important: we assume all logics we use are consistent and accept that they are incomplete.

More importantly, when talking about programs you actually get three choices, not two: "good", "bad", and "I don't know". Incompleteness means you cannot ever make an analysis that doesn't answer "I don't know" sometimes, but you can guarantee that your analysis is never wrong. If you are trying to verify something is safe, then you reject any programs that you get "I don't know" for along with any that can be verified as "bad", then you can be certain (modulo the correctness of your analysis which can be formally proven correct) that every program you say is "good" is actually good.

See Quark for a research prototype of a browser that is formally verified to have no security holes. There could still be a bug in the OS sandbox (uh, run it on seL4, I guess?) or, theoretically, in the theorem prover itself, but both are very unlikely. (The downsides of the current implementation are: (1) its security model is not precise enough to capture exactly how different domains are supposed to be allowed to interact and (2) is a slower than other browsers, although fast enough to run GMail and Facebook at acceptable speeds.)

You may not be able to just take any program and prove that it works, but you can construct a program of your own in a way that it is possible to prove that it works; actually what you do is the proof and then in best-case scenario extract the machine code from that.

Of course, doing this is still very costly: 7500 lines of C-code can take 200000 lines of Isabelle proof code:

    http://ertos.nicta.com.au/research/l4.verified/numbers.pml

Humans maybe, but why trust humans? Yes, that's only a kernel for now, but all systems start somewhere.

Insecurity in Public-Safety Communications: APCO Project 25

Abstract. APCO Project 25 (P25) radio networks are perhaps the most
widely-deployed digital radio technology currently in use by emergency
first-responders across the world. This paper presents the results of an
investigation into the security aspects of the P25 communication protocol.
The investigation uses a new software-defined radio approach to
expose the vulnerabilities of the lowest layers of the protocol stack. We
identify a number of serious security flaws which lead to practical attacks
that can compromise the confidentiality, integrity and availability of P25
networks.

...

Conclusions
P25 radio systems are more secure than conventional analogue radio systems
but not nearly as secure as the term “encrypted” would imply. The most serious
security flaw in P25 is the optional nature of the security protocol, however
even when the security protocol is used several serious security flaws present the
design of P25 cryptographic protections, remain:
– Weak encryption permits an attacker to recover the encryption key, and fre-
quent re-keying is not an effective defence.
Insecurity in APCO Project 25 17
– There is no effective authentication and access control mechanism.
– The lack of a key hierarchy means that a single key is used to encrypt traffic
between many users over many sessions.
– The integrity, authenticity and freshness of traffic cannot be ensured even
when the security protocol is in use.
– Serious denial-of-service threats against individual stations are possible.
The contribution of this paper is in several parts: firstly, we have applied the
techniques of software-defined radio to enable the study and network security
analysis. This approach has the potential to expose network traffic at all layers
of the protocol stack. Secondly we have identified a number of serious security
flaws that are present in the P25 protocol and described attacks which exploit
them.

Yeah, it was based on that but had formal proofs, I've been really interested in it but they're only releasing papers and the proofs about it. http://ertos.nicta.com.au/research/sel4/

Here's a link to implementation: http://ertos.nicta.com.au/research/l4.verified/

You can also check: http://en.wikipedia.org/wiki/Coyotos

Our embedded version of L4 was successfully commercialised, initially via direct engagement with QUALCOMM and other companies. This lead to spinning out our development team into the new company Open Kernel Labs (OK Labs). OK Labs has further developed L4-embedded into what is now called OKL4, and provides products and services based on this system.

Spin locks are flawed, hence the recent effort to replace them entirely with semaphores. User space library calls are equivalent to kernel space library calls (i.e. a call insn without a context switch). Zero copy buffers... is a valid argument, but arguable depending on kernel APIs and internals. Kernel tuning of whatever to a task is invalid for buffer sizes, and complex otherwise (specially tuning the scheduler?! That's a major operation). On Linux at least, X11 has had direct access to video memory since eternity, and I daresay direct PIO and MMIO to video chipset registers since God knows when.

Theoretical operating system design concepts are great, and most modern operating systems have glaring flaws. That said, most modern operating systems make theoretical operating system design classes look like medieval discussions on how to build a catapult... while you're busy cleaning your repeating rifle. It's not that the designers haven't made horrible errors that studying up a bit would make obvious; it's that the designers have also discovered errors in the theory, and based plenty enough of the design on new concepts that the system looks like black magic and future-ware.

While we're talking ARM, did you know L4 has an implementation with a few-microsecond context switch each way on ARM? L4 Wombat ARM bare context switch latency is on the order of microseconds; Linux context switching on the same ARM testing platform was on the order of hundreds of microseconds. The strange thing was the research effort that went into this was running tests on Linux, every time; L4 Wombat ARM is Linux ARM paravirtualized on L4 Pistachio. Some data here.

Granted there were some iffy issues like syscalls (major here) and fork() calls; but the bulk of effort is going to be a lot of work done to process (decompress) video, and shipping the decompressed data to the video processor. Likely the latter will be done with MMIO or PIO on a privilege mask; I understand these both exist on x86, I'm not sure about the ARM architecture though. Particularly, MMIO is a function of the MMU, and I believe ARM MMU specifics are variable (i.e. the MMU is a separate thing). These features would mitigate any concerns about shipping data from user space to the graphics chipset; but they may simply not exist on this architecture.

This is what you need our research for. We can actually work out when the best time to change to a lower FSB/memory/IO/CPU frequency is with one nice tunable like you're used to... http://ertos.nicta.com.au/research/power

The details are on NICTA's web site. Basically, they have verified that the C source code accurately implements a formal model of the L4 spec. They have not, for example, verified that the C compiler accurately implements the formal subset of C.

Formally verified compilers are still an active research area. Formally verified hardware has at least been around for a while, at least for chips smaller than VLSI.

What you'd like is for the entire stack to be formally verifiable, but we're a long way off that at the moment. Remember, it's only been in the last few years that assisted theorem provers like Isabelle and Coq have been up to the job.

There is a good overview of the topic on the authors page, at http://ertos.nicta.com.au/publications/papers/Klein_09.pdf. It specifically mentions "the other" big Project in this field, the VeriSoft project ( http://www.verisoft.de/ ). VeriSoft is broader in scope (covering the translation of programs down to machine code level, and also aiming to verify properties of user-space programs), but uses a simpler implementation Language lacking C-pointers, called "C0". C0 is extended with limited support for inline-assembly code for the compilation of the OS ( http://www-wjp.cs.uni-sb.de/publikationen/GHLP05.pdf ).

A lot of people here are saying: duh, they only proved that the C code has the same bugs as the formal specification.

But the researchers did consider that. The formal specification also allows them to prove important properties of the L4 kernel.

See the researcher's website: http://ertos.nicta.com.au/research/l4.verified/proof.pml

From the website:

Here, the absence of such bugs is just a useful by-product of the proof. To be able to complete our proof of functional correctness, we also prove a large number of so-called invariants: properties that we know to always be true when the kernel runs.

Before you get angry, I suggest you go read the page what we prove and what we assume. The researchers are not claiming the kernel is bug-free. They are saying that certain parts of the kernel are free from certain classes of errors so long as the rest of the system (the C compiler, the linker, the hardware, the boot code, assembly code related to direct hardware access, etc..) is working as designed.

As someone who has been doing Linux kernel programming for about 8 years, I enthusiastically support efforts to make a more robust operating system. Just being able to say "this chunk of C code doesn't have any null pointer dereferences" is a significant achievement (and incidentally, it's one of the reasons why I do all my "for fun" programming in Haskell and not in C; life is too short to spend tracking down type errors that would never have gotten past a decent compiler).

7500 lines of code is actually quite a lot. Mainstream OSes like Linux have much bigger code bases, but that's because they need to support as many hardware devices as possible, dozens of filesystems, many cpu architectures, work equally well on embedded devices and many-cpu NUMA machines, and support any feature anyone happens to want. If you just want a system that can run particular applications on a particular hardware platform, a significant amount of functionality can fit in 7500 lines of code.

but is the spec useable ? bugfree ?

Practical upshot seems to be that, yes, the spec could always be wrong, but once you've proven the code meets the specification, you can reliably "test" for bugs by further analysis of the spec*. Its worth scanning this part of TFA

where they discuss the limitations of what they have done. Key quote:

The C code of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more.

This sort of technique sounds ideally suited to microkernels which, by their nature (a) are tightly specified, and are supposed to eschew feeping creaturism (b) serve a technical audience (they're inmteracting almost exclusively with other software, so the "users" are really programmers) and (c) make minimal assumptions about any hardware other than the CPU.

That's valuable, but I think it will be a while yet before we see a formally proven web browser, or any other software with a direct meatspace interface...

...there are two caveats. One is that "executable specification in Haskell" is a bit of a dodge. It means that they have effectively verified the translation from Haskell to C, but if there are bugs in the Haskell then there will be bugs in the C as well (in fact this is part of what they've proven). They admit as much at the very top of http://ertos.nicta.com.au/research/l4.verified/proof.pml, but it still leaves the question of why this is any better than simply rewriting the microkernel in Haskell. If the benefit of a concise and abstract specification is lost, what's left?

The second major caveat is that they had to leave out some features that they couldn't verify. Most significant is that they didn't verify multi-core - by which it seems they mean multi-processor, but "multi-core" is the much hipper word. Since even laptops are multi-processor now, this limits applicability until they take the next step. With all of these shortcuts, though, if you look at the list of what they did manage to verify - mostly pointer errors and overflows - it's not clear that it couldn't have been done with a more real-code-oriented tool such as the Stanford Checker or sparse.

The missing word is formal.

They use a formal specification, which is then formally verified.

The overhead? It took something like 5 years for a 10,000 line program. The benefit is if the specification is right, the program should be right.

Other questions are answered in the FAQ linked in the summary and this page.

We did some work recently where we showed that in a lot of cases, running the CPU at a lower performance point actually resulted in more energy usage -- scaling down the CPU frequency means everything takes longer to run, which means that you get less time to spend in low-power idle modes. There are also a lot of other complexities with frequency scaling... Particularly on a platform like the Android where there would be multiple scalable frequencies, etc.

There's a whole lot of other problems with the slower-is-better approach... But check out the paper we've just published.

As a measure of QoS, I think this is quite cool work, but the way they translate this into frequency scaling seems broken.

Koala: A Platform for OS-Level Power Management

You need to run a 'nuclear launch control' ? http://www.ertos.nicta.com.au/research/sel4/

Maybe it could work, but Microsoft is a marketing-driven company and has failed to use good ideas their employees have had before. Similar ideas have been used in experimental operating systems before, such as L4 and Mungi. We do need innovation in operating systems, but unfortunately, Free and proprietary development seem equally slow to produce practical systems.

Thanks for the interesting link! Unfortunately, their work was entirely done on a now obsolete version of the kernel (2.4.18) and a request for comment on porting it to the 2.6 series was ignored by the hackers on LKML. A little more digging found the probable reason: the system has a number of problems. In particular, this paper by Peter Chubb from the University of New South Wales (pdf) outlined some of the issues (pp 2-3, emphasis added):

The Nooks work [Swift et al., 2002] showed that by isolating drivers from the kernel address space, the most common programming errors could be made recoverable. In Nooks, drivers are insulated from the rest of the kernel by running each in a separate address space, and replacing the driver/kernel interface with a new one that uses cross-domain procedure calls to replace any procedure calls in the ABI, and that creates shadow copies of any shared variables in the protected address space.

This approach provides isolation, but also has problems: as the driver model changes, there is quite a lot of wrapper code that has to be changed to accommodate the changed APIs. Also, the value of any shared variable is frozen for the duration of a driver ABI call. The Nooks work is uniprocessor only; locking issues therefore have not yet been addressed.

That obviously is a bit of a show-stopper, as SMP and hyperthreaded systems are becoming more and more common in practice; it's not clear how complex extending the Nooks system would be. But the paper I linked actually suggests that for most drivers, there's no need to have them in kernel space at all: with a little bit of work, it seems that "almost any PCI bus-mastering device could have a user mode device driver." (ibid)

It's an interesting read, if you have a moment I recommend you take a look.

I still think using a microkernel would be best, and the L4 people have shown that a properly implemented microkernel can be nearly as fast as a macrokernel -- turns out (surprise surprise) that it's Mach that's given the microkernel a bad name. But the complexity issue remains daunting, and that (along with an unreasonable political attachment to Mach) has kept the L4-Hurd project from really getting off the ground. It's a shame.

already been done: http://www.warren.usyd.edu.au/bulletin/NO49/ed49ar t3.htm, http://nicta.com.au/uploads/documents/060915_audie nceresponse_casestudy.pdf

From http://www.ertos.nicta.com.au/software/kenge/womba t/latest/
Wombat is "A port of linux to run on top of L4/Iguana"

Just to clarify that the post makes it sound like they are switching away from linux.

G'Day,

Linux itself has a number of issues which have been outlined in various other comments. Lack of proper real-time support, speed on ARM, reliability and security. While these probably limit how useful Linux can be, there is a solution being developed. Two companies in particular are building it: Jaluna and ERTOS at NICTA. That solution is para-virtualising linux on top of a fast, real-time, and secure operating system. Performance, I hear you say? The ERTOS solution is so fast that in some cases it out-performs native linux, and in most others performs comparably. These systems have already started to make it into mobile phone manufacturer's hands

Dave.

National ICT Australia is a new research organisation set up by the government to work on "use-inspired" research. They're a nice combination between academia and industry. While CSIRO is a general science research organisation, NICTA is focussed on ICT. I work for the Embedded Real-time and Operating systems group within NICTA, and (with all modesty) we're doing some kick-arse stuff (focussing on seriously fast microkernels, virtualisation, power management, etc) with a very smart group of people. Our research is starting to make it into industry, with our software being used in Qualcomm platforms. There's too much stuff to write about here, but have a look at the website and, even with a moderate appreciation for OS technology, you'll be impressed. Other groups within NICTA are also doing some interesting things, but I don't know so much about them.

National ICT Australia is a new research organisation set up by the government to work on "use-inspired" research. They're a nice combination between academia and industry. While CSIRO is a general science research organisation, NICTA is focussed on ICT. I work for the Embedded Real-time and Operating systems group within NICTA, and (with all modesty) we're doing some kick-arse stuff (focussing on seriously fast microkernels, virtualisation, power management, etc) with a very smart group of people. Our research is starting to make it into industry, with our software being used in Qualcomm platforms. There's too much stuff to write about here, but have a look at the website and, even with a moderate appreciation for OS technology, you'll be impressed. Other groups within NICTA are also doing some interesting things, but I don't know so much about them.

As a Darbat (L4/Darwin) developer this is sad, and will be a bit of a set-back. We were hoping to try and become involved with the OpenDarwin community. I'm really sorry to see that this really handy resource will be going.

But the AIM7 benchmark, which models typical general-purpose Unix system usage, has consistently faster results for regular Linux than for the Wombat virtualized version, even though there may be individual functions that are faster. The cool thing, though, is that the performance hit is only about 2-3% - not bad at all for a microkernel with some provable security and reliability features.

Its performance has nothing to do with being microkernel. TFA claims its better performance is because of the FASS (Fast Address-Space Switching) technology that has been implemented on the Linux too. Its dependent on the ARM architecture and I guess is not applicable in other architectures.

NICTA is pretty good about a sense of humour, in one of their Darbat SConstruct files (scons is a miserable build system, like GNU/Make but with much less cowbell) they have the following at the top of the file:

SetOption('implicit_cache', 0)
#blah
"""
AHRRRRRRRR!
"""
Import("*")

Rumour has it, it's to make scons work correctly, oops.

I've been researching more and more into NICTA's microkernel and virtualization (for my L4::BSD idea) and one thing that is important to understand is that NICTA's development is mainly on ARM, the Kenge toolset, as well as the Iguana OS are both much further along on ARM as opposed to i386

Considering the work that NICTA does with companies that produce embedded hardware like Qualcomm, this isn't surprising, but don't go crazy about this.

Linux development is much more fine tuned on x86, and Kenge/Iguana development is much more fine tuned on ARM; no need to start holy wars here ;)

That said, nice work benno, chuck, and gernot (and whomever else I'm forgetting)

The result is that context-switching costs of virtualised Linux are up to thirty times less than in native Linux.

In any case, as there are more embedded devices willing to run opensource software than PCs and servers, I'd say that those results are very good!
And maybe there will be a way to embed that technology into Linux!

In any case, as there are more embedded devices willing to run opensource software than PCs and servers, I'd say that those results are very good!
And maybe there will be a way to embed that technology into Linux!

In any case, as there are more embedded devices willing to run opensource software than PCs and servers, I'd say that those results are very good!
And maybe there will be a way to embed that technology into Linux!

Could it be because linux for ARM is not that well optimised . I can't imagine such massive performance gains otherwise , bar a massive bug in the kernel.

Fast Address-Space Switching for ARM Linux Kernels

The Fast Address-Space Switching (FASS) project aims to utilise some of the features of the Memory Management Unit in the ARM architecture to improve the performance of context switches under the L4 kernel and ARM Linux.

Ignore the second link. The actual performance results are here.

I have yet to see a "proper" non-academic microkernel which lets one part fail while the rest remain

Have a look at the Iguana and Wombat projects. They use the L4 microkernel for OS virtualization in embedded systems (most notably in Linux based phones).

I have yet to see a "proper" non-academic microkernel which lets one part fail while the rest remain

Have a look at the Iguana and Wombat projects. They use the L4 microkernel for OS virtualization in embedded systems (most notably in Linux based phones).

Coincidently, I was just looking at virtualization options for Linux but for embedded devices. I came across Iquana (http://www.ertos.nicta.com.au/software/kenge/igua na-project/latest/), which I consider very interesting.