Slashdot Mirror
Domain: nicta.com.au
Stories and comments across the archive that link to nicta.com.au.
Stories · 6
-
Ask Slashdot: When and How To Deal With GPL Violations?
jd writes "There are many pieces of software out there, such as seL4 (kindly brought to my attention by another reader), where the vendor has indeed engineered something that they're entitled to Close Source, but where their closed-source license includes the modifications to GPLed software such as the Linux kernel. Then there's a second type of behavior. Code Sourcery produced two versions of their VSIPL++ image processing library — one closed-source, one GPLed. It was extremely decent of them. When Mentor Graphics bought Code Sourcery, they continued developing the closed-course one and discontinued, then deleted, the GPL variant. It's unclear to me if that's kosher, as the closed variant must contain code that had been GPLed at one point. Here's the problem: complaining too much will mean we get code now that maybe four or five people, tops, will actually care about. It will also make corporations leery of any other such work in future, where that work will be of greater value to a greater number of people. So, the question I want to ask is this: When is it a good time to complain? By what rule-of-thumb might you decide that one violation is worth cracking down on, and another should be let go to help encourage work we're never going to do ourselves?" -
Security Researchers Crack APCO P25 Encryption
An anonymous reader writes "Two Australian security researchers, Stephen Glass and Matt Robert, have published a paper that details flaws in the encryption implementation (PDF) in the APCO Project 25 digital radio standard, used by emergency services and police departments world-wide. The paper details flaws in the DES-OFB and ADP encryption that enable the encryption key to be recovered by traditional brute force key searching. Also detailed is a DoS attack that makes use of unauthenticated radio inhibit mechanism. The research is part of the OP25 project, which uses GNUradio to implement a P25 stack using software defined radio. With this solution in place, the researchers were able to do detailed analysis of the traffic coming from various radio systems and to transmit and receive to P25 radios in their lab." -
World's First Formally-Proven OS Kernel
An anonymous reader writes "Operating systems usually have bugs — the 'blue screen of death,' the Amiga Hand, and so forth are known by almost everyone. NICTA's team of researchers has managed to prove that a particular OS kernel is guaranteed to meet its specification. It is fully, formally verified, and as such it exceeds the Common Criteria's highest level of assurance. The researchers used an executable specification written in Haskell, C code that mapped to Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system." Does it run Linux? "We're pleased to say that it does. Presently, we have a para-virtualized version of Linux running on top of the (unverified) x86 port of seL4. There are plans to port Linux to the verified ARM version of seL4 as well." Further technical details are available from NICTA's website. -
World's First Formally-Proven OS Kernel
An anonymous reader writes "Operating systems usually have bugs — the 'blue screen of death,' the Amiga Hand, and so forth are known by almost everyone. NICTA's team of researchers has managed to prove that a particular OS kernel is guaranteed to meet its specification. It is fully, formally verified, and as such it exceeds the Common Criteria's highest level of assurance. The researchers used an executable specification written in Haskell, C code that mapped to Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system." Does it run Linux? "We're pleased to say that it does. Presently, we have a para-virtualized version of Linux running on top of the (unverified) x86 port of seL4. There are plans to port Linux to the verified ARM version of seL4 as well." Further technical details are available from NICTA's website. -
Solar Powered Car Attempts to Break Record
Snowdon writes "Jaycar Sunswift III today started on its 4000km journey across the Australian outback, in an attempt to beat the 8.5 day record from Perth to Sydney. The team expects to complete the journey in 6 days, depending on the weather. It is a seriously innovative machine, with the aerodynamic design iteratively optimised on 80 CS lab computers over three months, custom-built carbon-fibre wheels, chassis, suspension and steering components, and custom-built power electronics and telemetry/control systems (components of which presently use Linux, but will soon run Iguana/Wombat). It is the result of several years' work by both undergraduate and postgraduate students at UNSW. Keep track of the team's progress by visiting www.sunswift.com." -
Virtualized Linux Faster Than Native?
^switch writes "Aussies at NICTA have developed a para-virtualized Linux called Wombat that they claim outperforms native Linux. From the article: 'The L4 Microkernel works with its own open source operating system Iguana, which is specifically designed as a base for use in embedded systems.'" Specific performance results are also available from the NICTA website.