Раздел: Спорт
Нові технології — Вчені створили безпечне ядро операційної системи
Автор: nest
Дата: 07.11.2024
Австралійські вчені створили мікроядро операційної системи, відсутність в якому різних типів помилок, підтверджена математично. Ця розробка спрямована на створення "безпечного програмного забезпечення безпрецедентного рівня надійності" для літаків та автомобілів.
Створене командою центру NICTA (Information and Communications Technology Centre of Excellence) мікроядро отримало назву "secure embedded L4" (seL4). За словами вчених, воно являє собою перший "зразок ядра операційної системи загального призначення, який пройшов сувору машинну перевірку".
За підсумками чотирьох років роботи було написано і перевірено 7500 рядків коду мовою C. В ході перевірок розробники довели понад 10 000 проміжних теорем, написали більше двохсот тисяч рядків чітких доведень, які потім були перевірені з використанням інтерактивної програми Isabelle, призначеної спеціально для доведення теорем.
Вся ця клопітка математична робота означає, що створене ядро повинно мати імунітет до поширених типів атак, таких як переповнення буферу. Дана розробка - приклад найбільш ранніх проектів, однак вчені мають намір рухатися далі.
За словами головного наукового співробітника NICTA, доктора Гервіна Кляйна, раніше досліди такого роду були направлені на перевірку окремих компонентів програмного забезпечення, однак на цей раз його команді вдалося розробити цілісну методику перевірки загального призначення, створену спеціально для складного і високопродуктивного ПЗ, чого раніше не вдавалося домогтися нікому.
NICTA планує передати інтелектуальні права на свою розробку фірмі Open Kernel Labs, яка розробляє гіпервізори для віртуалізації.
Назад
Комментариев:
0
Просмотров:
960
Додавати коментарі можуть лише зареєстровані користувачі.
[
Реєстрація |
Вхід ]