Mutation testing of access control policies

Abstract

One of the most important and integral components of modern computer security are access control systems. The objective of an access control system (ACS) is often described in terms of protecting system resources against inappropriate or unwanted user access. However, a large degree of sharing can interfere with the protection of resources, so a sufficiently detailed AC policy should allow selective exchange of information when, in its absence, sharing can be considered too risky in general. Erroneous configurations, faulty policies, as well as flaws in the implementation of software can lead to global insecurity. Identifying the differences between policy specifications and their inten ded functions is crucial because the correct implementation and enforcement of the policies of a particular application is based on the premise that the specifications of this policy are correct. As a result of the policy, the specifications presented by the models must undergo rigorous validation and legalization through systematic checks and tests to ensure that the specifications of the policies really correspond to the wishes of the creators. Verifying that access control policies and models are consistent is not a trivial and critical task. And one of the important aspects of such a check is a formal check for inconsistency and incompleteness of the model, and the security requirements of the policy, because the access control model and its implementation do not necessarily express policies that can also be hidden, embedded by mixing with direct access restrictions or another access control model.

Одними з найскладніших, важливих та невід'ємних складових сучасної комп'ютерної безпеки є системи керування доступу. Завдання системи керування доступом часто описується з точки зору захисту ресурсів системи проти невідповідного або небажаного доступу користувача. Проте, велика ступінь спільного використання може перешкодити захисту ресурсів, таким чином, досить детальна політика керування доступом повинна дозволяти виборчий обмін інформацією, коли в його відсутність, спільне використання може вважатися занадто ризикованим в цілому. Помилкові конфігурації, несправні політики, а так само недоліки в реалізації програмного забезпечення можуть призвести до глобальної незахищеності. Виявлення відмінностей між специфікаціями політик і їх передбачуваними функціями має вирішальне значення, тому що правильна реалізація і забезпечення дотримання політик конкретного додатка засновані на передумові, що специфікації даної політики є правильними. В результаті політики специфікації, представлені моделями, повинні пройти сувору перевірку і легалізацію шляхом систематичних перевірок і тестувань, щоб гарантувати, що специфікації політик дійсно відповідають бажанням творців. Перевірка відповідності політик і моделей контролю доступу нетривіальна і критична завдання. І одним з важливих аспектів такої перевірки є формальна перевірка на непослідовність і неповноту у моделі, і вимоги безпеки політики, тому що модель контролю доступу та її реалізація не обов'язково явно виражають політики, які також можуть бути приховані, вбудовані шляхом змішування з обмеженнями прямого доступу або іншого доступу моделі управління.