х систем з високими вимогами надійності. Щоб виявити найбільшу кількість помилок, слід застосовувати всебічне тестування, а при оцінці безпеки використовувати статичні методи тестування. Однак внаслідок надзвичайно низької частоти відмов, властивих багатьом КС, за допомогою статичного тестування не завжди вдається кількісно оцінити безвідмовність, так як для цього потрібно дуже велике число тестів. Ці тести лише дають підставу вважати ту чи іншу КС безпечною.
При створенні КС, важливий всебічний аналіз розроблюваної системи. Є п'ять типів аналізу системи, обов'язкових для КС:
. Аналіз правильності функціонування системи
. Аналіз можливості зміни і зрозумілості системної архітектури
. Аналіз відповідності алгоритму обробки і структури даних певному в специфікації поведінки системи
. Аналіз узгодженості програмного коду, алгоритмів і структур даних.
. Аналіз адекватності тестових сценаріїв системним вимогам.
Усі докази безпеки системи будуються на наступному припущенні: кількість помилок у системі, які призводять до аварійних ситуацій, набагато менше загального числа помилок в системі. Забезпечення безпеки має зосередитися на виявленні потенційно небезпечних помилок. Якщо виявляється, що ці помилки не виявляються або виявляються, але не призводять до серйозних наслідків, то система вважається надійною. Докази правильності програм були запропоновані в якості методів верифікації ПЗ більше 25 років тому. Однак ці методи в основному використовуються тільки в лабораторіях. Практичні проблеми побудови докази правильності ПО настільки складні, що деякі організації вважають використання даних методів у процесі розробки звичайних систем невиправдано дорогим. Але, як зазначалося раніше, для ряду КС економічно вигідно використовувати докази правильності системи, ніж ліквідувати наслідки відмов. Незважаючи на те, що для більшості систем розробляти докази правильності нерентабельно, іноді виникає необхідність розробити докази безпеки, що демонструють відповідність даної програми вимогам щодо забезпечення безпеки. При доказі безпеки необов'язково доводити відповідність програми специфікації. Необхідно тільки показати, що виконання програми не призводить до збоїв з небезпечними наслідками.
Висновок
У цій роботі були розглянуті питання верифікації та атестації ПЗ. Було виявлено, що це дуже складні кроки в розробці будь-якого продукту, що вимагають від інженерів уваги, найвищої кваліфікації, терпіння, а від організації - великих вкладень коштів. Однак якими б дорогими були ці процеси, економічна вигода від їх використання очевидна, адже система без збоїв не завдає збитків. Слід пам'ятати, що аварійні ситуації - рідкісні події (особливо в КС), тому практично неможливо змоделювати їх під час тестування системи. Було встановлено, що вимоги безпеки ніколи не виключають ненадійного поведінки системи. За допомогою тестування та інших процесів атестації неможливо повністю довести відповідність системи вимогам безпеки. Верифікація та атестація повинні стати обов'язковими кроками в розробці ПЗ, нехай навіть самого простого. Кожна компанія, що виробляє ПЗ, повинна створити штат співробітників, які будуть займатися тільки верифікацією та атестацією: це інженери-тестери, інженери-іспектор та ін Організ...
