Вчені створили безпечне ядро операційної системи Автор: Вікторія · Опубліковано: 19.08.2009 12:22 · Розділ: Нові технології

Австралійські вчені створили мікроядро операційної системи, відсутність в якому різних типів помилок, підтверджена математично. Ця розробка спрямована на створення "безпечного програмного забезпечення безпрецедентного рівня надійності" для літаків та автомобілів.

Створене командою центру NICTA (Information and Communications Technology Centre of Excellence) мікроядро отримало назву "secure embedded L4" (seL4). За словами вчених, воно являє собою перший "зразок ядра операційної системи загального призначення, який пройшов сувору машинну перевірку".

За підсумками чотирьох років роботи було написано і перевірено 7500 рядків коду мовою C. В ході перевірок розробники довели понад 10 000 проміжних теорем, написали більше двохсот тисяч рядків чітких доведень, які потім були перевірені з використанням інтерактивної програми Isabelle, призначеної спеціально для доведення теорем.

Вся ця клопітка математична робота означає, що створене ядро повинно мати імунітет до поширених типів атак, таких як переповнення буферу. Дана розробка - приклад найбільш ранніх проектів, однак вчені мають намір рухатися далі.

За словами головного наукового співробітника NICTA, доктора Гервіна Кляйна, раніше досліди такого роду були направлені на перевірку окремих компонентів програмного забезпечення, однак на цей раз його команді вдалося розробити цілісну методику перевірки загального призначення, створену спеціально для складного і високопродуктивного ПЗ, чого раніше не вдавалося домогтися нікому.

NICTA планує передати інтелектуальні права на свою розробку фірмі Open Kernel Labs, яка розробляє гіпервізори для віртуалізації.

Джерело xakep.ru


Інші новини розділу

  • Цікаві факти про компресор

    Цікаві факти про компресор · Jane Holiday · 19.05.2017 12:02

    Компресор – це енергетична машина чи пристрій для підвищення тиску (стискання) та переміщення газоподібних речовин. «Батьком» компресора був насос, він винайдений тисячу років тому. Зараз вони використовуються в найрізноманітніших галузях промисловості.


  • Стиснене повітря - новий спосіб збереження енергії

    Стиснене повітря - новий спосіб збереження енергії · kseniya_www · 15.04.2017 21:14

    Канадська компанія Hydrostor розробила нову систему зберігання енергії на основі стисненого повітря, яка дешевша літій-іонних акумуляторних батарей, а також не використовує природний газ, як це роблять інші системи такого типу.


  • 2017: найочікуваніші гаджети

    2017: найочікуваніші гаджети · Anastasia · 16.01.2017 10:19

    Минулий рік не відзначився революційними новинками у сфері широкого вжитку. Прозорі чи гнучкі смартфони не з’явилися на ринку, а гаджети, які працюють за допомогою безпровідної зарядки акумулятора, без сумніву потрібно вдосконалювати. Також відкритим залишається питання про заряд звичних акумуляторів, які при інтенсивному використанні смартфону працюють не більше одного дня. До вашої уваги підбірка апаратів, які будуть конкурувати на ринку і зацікавлять суспільство у 2017.


  • Найкращі технологічні новинки 2016

    Найкращі технологічні новинки 2016 · Anastasia · 09.01.2017 13:35

    Минулий рік видався багатим на техно-новинки в сфері віртуальної реальності та використання дронів. Не менш важливим є представлення концепту «сонячного даху», що у майбутньому дасть можливість позбавитися електроенергії. Інтенсивність розвитку саме цих відгалужень зумовлена в першу чергу потребою людства у збереженні екологічної системи нашої планети.


  • Як вибрати праску?

    Як вибрати праску? · Anastasia · 04.01.2017 17:06

    Вдома ми користуємося багатьма гаджетами, які спрощують нам життя і допомагають виглядати на всі сто. Тому при виборі праски для домашнього вжитку ще в магазині слід звертати увагу на такі дрібниці як поверхня, якість ручки та допоміжні деталі. Далі декілька корисних порад, щоб обрати найоптимальніший варіант за співвідношенням ціна - якість.