Категорії розділу
| Спорт [122] |
| Комп'ютери [34] |
| Ігри [85] |
| Освіта [38] |
| Політика [54] |
| Кіно [55] |
| В Росії [20] |
| В світі [79] |
| Економіка [46] |
| Зірок Світу [43] |
| PC Ігри [11] |
| Онлайн игры [30] |
Силки
Популярное
| [18.01.2009] | [Кіно] |
| Умер агент 006 (0) | |
| [17.01.2009] | [Політика] |
| Кабмін ініціює створення компаній-постачальників газу в регіонах (0) | |
| [24.01.2009] | [Спорт] |
| Эрик Жерес хотел бы видеть в "Марселе" форварда донецкого "Шахтёра" (0) | |
| [11.01.2009] | [Економіка] |
| Кремль: Газова криза спеціально спровокована Києвом (0) | |
| [17.01.2009] | [В світі] |
| Тимошенко придумала новий спосіб забезпечити українців газом (0) | |
Авторизация
Чат
Опрос
Допомога
Якщо вам подобаеться
цей проект то ви можете
розмістити цю кнопку,
тим самим домоможете
проекту.Просто скопіруйте ниже код.
Статистика
Онлайн всього: 1
Гостей: 1
Користувачів: 0
» Зарег. на сайте
Всего: 93
Новых за месяц: 0
Новых за неделю: 0
Новых вчера: 0
Новых сегодня: 0
» Из них
Администраторов: 1
Модераторов: 0
Всего: 93 Новых за месяц: 0 Новых за неделю: 0 Новых вчера: 0 Новых сегодня: 0 » Из них
Администраторов: 1 Модераторов: 0
Проверенных: 3 
Обычных юзеров: 89 » Из них
Парней: 56 
Девушек: 37 
Будьласка натисніть нижще наведену картинку та силку.Зараніє Дякую!
Раздел: Спорт
Нові технології — Вчені створили безпечне ядро операційної системи
Австралійські вчені створили мікроядро операційної системи, відсутність в якому різних типів помилок, підтверджена математично. Ця розробка спрямована на створення "безпечного програмного забезпечення безпрецедентного рівня надійності" для літаків та автомобілів.
Створене командою центру NICTA (Information and Communications Technology Centre of Excellence) мікроядро отримало назву "secure embedded L4" (seL4). За словами вчених, воно являє собою перший "зразок ядра операційної системи загального призначення, який пройшов сувору машинну перевірку".
За підсумками чотирьох років роботи було написано і перевірено 7500 рядків коду мовою C. В ході перевірок розробники довели понад 10 000 проміжних теорем, написали більше двохсот тисяч рядків чітких доведень, які потім були перевірені з використанням інтерактивної програми Isabelle, призначеної спеціально для доведення теорем.
Вся ця клопітка математична робота означає, що створене ядро повинно мати імунітет до поширених типів атак, таких як переповнення буферу. Дана розробка - приклад найбільш ранніх проектів, однак вчені мають намір рухатися далі.
За словами головного наукового співробітника NICTA, доктора Гервіна Кляйна, раніше досліди такого роду були направлені на перевірку окремих компонентів програмного забезпечення, однак на цей раз його команді вдалося розробити цілісну методику перевірки загального призначення, створену спеціально для складного і високопродуктивного ПЗ, чого раніше не вдавалося домогтися нікому.
NICTA планує передати інтелектуальні права на свою розробку фірмі Open Kernel Labs, яка розробляє гіпервізори для віртуалізації.
Створене командою центру NICTA (Information and Communications Technology Centre of Excellence) мікроядро отримало назву "secure embedded L4" (seL4). За словами вчених, воно являє собою перший "зразок ядра операційної системи загального призначення, який пройшов сувору машинну перевірку".
За підсумками чотирьох років роботи було написано і перевірено 7500 рядків коду мовою C. В ході перевірок розробники довели понад 10 000 проміжних теорем, написали більше двохсот тисяч рядків чітких доведень, які потім були перевірені з використанням інтерактивної програми Isabelle, призначеної спеціально для доведення теорем.
Вся ця клопітка математична робота означає, що створене ядро повинно мати імунітет до поширених типів атак, таких як переповнення буферу. Дана розробка - приклад найбільш ранніх проектів, однак вчені мають намір рухатися далі.
За словами головного наукового співробітника NICTA, доктора Гервіна Кляйна, раніше досліди такого роду були направлені на перевірку окремих компонентів програмного забезпечення, однак на цей раз його команді вдалося розробити цілісну методику перевірки загального призначення, створену спеціально для складного і високопродуктивного ПЗ, чого раніше не вдавалося домогтися нікому.
NICTA планує передати інтелектуальні права на свою розробку фірмі Open Kernel Labs, яка розробляє гіпервізори для віртуалізації.
| Всього коментарів: 0 | |
Украинская Баннерная Сеть
