Code breakthrough delivers safer computing
September 25, 2009(PhysOrg.com) -- Computer researchers at UNSW and NICTA have achieved a breakthrough in software which will deliver significant increases in security and reliability and has the potential to be a major commercialisation success.
Professor Gernot Heiser, the John Lions Chair in Computer Science in the School of Computer Science and Engineering and a senior principal researcher with NICTA, said for the first time a team had been able to prove with mathematical rigour that an operating-system kernel - the code at the heart of any computer or microprocessor - was 100 per cent bug-free and therefore immune to crashes and failures.
The breakthrough has major implications for improving the reliability of critical systems such as medical machinery, military systems and aircraft, where failure due to a software error could have disastrous results.
“A rule of thumb is that reasonably engineered software has about 10 bugs per thousand lines of code, with really high quality software you can get that down to maybe one or three bugs per thousand lines of code,” Professor Heiser said.
“That can mean there are a lot of bugs in a system. What we’ve shown is that it’s possible to make the lowest level, the most critical, and in a way the most dangerous part of the system provably fault free.”
“I think that’s not an exaggeration to say that really opens up a completely new world with respect to building new systems that are highly trustworthy, highly secure and safe.”
Verifying the kernel - known as the seL4 microkernel - involved mathematically proving the correctness of about 7,500 lines of computer code in an project taking an average of six people more than five years.
“The NICTA team has achieved a landmark result which will be a game changer for security-and-safety-critical software,” Professor Heiser said.
“The verification provides conclusive evidence that bug-free software is possible, and in the future, nothing less should be considered acceptable where critical assets are at stake.”
-
Software 'Chipper' Speeds Debugging
Oct 01, 2007 |
not rated yet |
0
-
IBM Debuts 'Grammar Checker' Approach to Catching Software Bugs
Jul 30, 2008 |
not rated yet |
0
-
New tool improves productivity, quality when translating software
Feb 24, 2009 |
not rated yet |
0
-
Serious Samba Problems
May 17, 2007 |
not rated yet |
0
-
Software industry's 'patch culture' attack
Jun 06, 2006 |
not rated yet |
0
-
Engineers build first sub-10-nm carbon nanotube transistor
Feb 01, 2012 |
4.9 / 5 (28) |
26
-
Something old, something new: Evolution and the structural divergence of duplicate genes
Jan 31, 2012 |
4.6 / 5 (7) |
1
-
The hidden nanoworld of ice crystals: Revealing the dynamic behavior of quasi-liquid layers
Jan 30, 2012 |
5 / 5 (3) |
1
-
Stock market network reveals investor clustering
Jan 27, 2012 |
4 / 5 (22) |
8
-
Of microchemistry and molecules: Electronic microfluidic device synthesizes biocompatible probes
Jan 26, 2012 |
5 / 5 (1) |
0
-
Synergistic relations between computer science and technology.
Feb 06, 2012
-
how do iphone gloves work?
Feb 05, 2012
-
iPhone battery over time
Jan 30, 2012
-
Best alternate Tablet to an iPad for writing math or physics equations?
Jan 26, 2012
-
Sending SMS to a website
Jan 20, 2012
-
Need help with my technical fest!
Jan 19, 2012
- More from Physics Forums - Computing & Technology
More news stories
Nicira promises virtual networks will transform networking
(PhysOrg.com) -- For the past four years, founders of the start-up company Nicira have been developing cutting-edge software that they predict will transform the networking technology underlying the Internet. ...
Navy to begin tests on electromagnetic railgun prototype launcher
The Office of Naval Research (ONR)'s Electromagnetic (EM) Railgun program will take an important step forward in the coming weeks when the first industry railgun prototype launcher is tested at a facility ...
11 hours ago |
4.4 / 5 (9) |
38
|
After Megaupload closure, BTJunkie shuts down
BTJunkie, a popular file-sharing indexing site, said Monday it was voluntarily shutting down, less than three weeks after the US closure of Megaupload in a crackdown on piracy of music, films and other materials.
11 hours ago |
5 / 5 (3) |
6
Bigger US role against companies' cyberthreats?
(AP) -- A developing Senate plan that would bolster the government's ability to regulate the computer security of companies that run critical industries is drawing strong opposition from businesses that say ...
14 hours ago |
5 / 5 (2) |
6
Solvay hails world's largest fuel cell of type in Flanders, one can power 1,400 homes
Chemicals giant Solvay hailed Monday the successful entry into service in Flanders of what it said was the largest fuel cell of its type in the world.
Technology / Energy & Green Tech
15 hours ago |
4.6 / 5 (5) |
5
Study of diving beetles suggest sperm evolution may be driven by changes in female reproductive organs
Studying female reproductive tracts and sperm in diving beetles (Dytiscidae), researchers from the University of Arizona and Syracuse University have obtained a glimpse into a bizarre and amazing world of spe ...
Fossil cricket: Jurassic love song reconstructed
Some 165 million years ago, the world was host to a diversity of sounds. Primitive bushcrickets and croaking amphibians were among the first animals to produce loud sounds by stridulation (rubbing certain body parts together). ...
New insight from whole-genome sequencing of Europe's 2011 E. coli outbreaks
Using whole-genome sequencing, a team led by researchers from Harvard School of Public Health (HSPH) and the Broad Institute has traced the path of the E. coli outbreak that sickened thousands and killed over 50 people in Ger ...
Redder ladybirds more deadly, say scientists
A ladybird's colour indicates how well-fed and how toxic it is, according to an international team of scientists. Research led by the Universities of Exeter and Liverpool directly shows that differences between ...
Russia 'drills into' Antarctic subglacial lake
A Russian team has succeeded in drilling through four kilometres (2.5 miles) of ice to the surface of a mythical subglacial Antarctic lake which could hold as yet unknown life forms, reports said Monday.
Harnessing plasmonics, engineers weld nanowires with light
At the nano level, researchers at Stanford have discovered a new way to weld together meshes of tiny wires. Their work could lead to exciting new electronics and solar applications. To succeed, they called ...
Sep 25, 2009
Rank: not rated yet
Considering the efforts of this team, how much effort would be required to verify a complete operating system, and then the productivity software that we use to do our day-to-day work?
It took 30 work-years to verify just this 7500 line module - albeit the most critical module. But that number of lines is laughable in consideration of a single software product, such as an office application. How can consumers be informed of the quality of the software they purchase, if the verification process renders the software obsolete before it can reach the market?
Or is this kernal exclusively for laboratories, and its verification process a once only event?