Systém typu zabezpečení - Security type system

Tento článek obsahuje a seznam doporučení, související čtení nebo externí odkazy, ale jeho zdroje zůstávají nejasné, protože mu chybí vložené citace. Prosím pomozte zlepšit tento článek představuji přesnější citace. (Červenec 2020) (Zjistěte, jak a kdy odstranit tuto zprávu šablony)

v počítačová věda, a typový systém lze popsat jako syntaktický rámec, který obsahuje sadu pravidel, která se používají k přiřazení vlastnosti typu (int, boolean, char atd.) různým komponentám počítačového programu, jako jsou proměnné nebo funkce. A systém typu zabezpečení funguje podobným způsobem, pouze s hlavním zaměřením na bezpečnost počítačového programu, prostřednictvím informační tok řízení. Tudíž různým součástem programu jsou přiřazeny typy zabezpečení nebo štítky. Cílem takového systému je nakonec být schopen ověřit, zda daný program odpovídá pravidlům typového systému a vyhovuje nevměšování. Systémy typu zabezpečení jsou jednou z mnoha bezpečnostních technik používaných v oblasti jazykové zabezpečení a je úzce spojen s tokem informací a politikami toku informací.

Jednoduše řečeno, systém typu zabezpečení lze použít k detekci, zda existuje nějaký druh narušení důvěrnost nebo integrita v programu, tj. programátor chce zjistit, zda je program v souladu se zásadami toku informací nebo ne.

Jednoduchá politika toku informací

A Hasseův diagram, popisující jednoduchou zásadu toku informací o důvěrnosti.

Předpokládejme, že existují dva uživatelé, A a B. V programu následující třídy zabezpečení (SC) se zavádějí:

• SC = {∅, {A}, {B}, {A, B}}, kde ∅ je prázdná množina.

Zásada toku informací by měla definovat směr, kterým mohou informace plynout, což závisí na tom, zda to politika umožňuje číst nebo psát si operace. Tento příklad uvažuje číst operace (důvěrnost). Jsou povoleny následující toky:

• → = {({A}, {A}), ({B}, {B}), ({A, B}, {A, B}), ({A, B}, {A}), ( {A, B}, {B}), ({A}, ∅), ({B}, ∅), ({A, B}, ∅)}

To lze také popsat jako nadmnožinu (⊇). Slovy: informace mohou proudit směrem k přísnějším úrovně důvěrnosti. Operátor kombinace (⊕) může vyjádřit, jak mohou třídy zabezpečení provádět operace čtení s ohledem na jiné třídy zabezpečení. Například:

• {A} ⊕ {A, B} = {A} - jediná třída zabezpečení, která umí číst z obou {A} a {A, B} je {A}.
• {A} ⊕ {B} = ∅ - ani {A} ani {B} mohou číst z obou {A} a {B}.

To lze také popsat jako průnik (∩) mezi třídami zabezpečení.

Zásadu toku informací lze ilustrovat jako a Hasseův diagram. Tato politika by měla být také a mříž, to znamená, že má největší dolní a nejnižší horní mez (vždy existuje kombinace mezi třídami zabezpečení). V případě integrity budou informace proudit opačným směrem, takže politika bude obrácena.

Zásady toku informací v systémech typu zabezpečení

Jakmile jsou zásady zavedeny, může vývojář softwaru použít třídy zabezpečení na součásti programu. Použití systému typu zabezpečení je obvykle kombinováno s překladačem, který může provádět ověření toku informací podle pravidel systému typu. Z důvodu jednoduchosti lze jako ukázku použít velmi jednoduchý počítačový program spolu se zásadami toku informací popsanými v předchozí části. Jednoduchý program je uveden v následujícím pseudokódu:

pokud y{A} = 1 pak x{A, B} : = 0 jinak x{A, B} := 1

Zde se provádí kontrola rovnosti u proměnné y, které je přiřazena třída zabezpečení {A}. Proměnná x s nižší bezpečnostní třídou ({A, B}) je touto kontrolou ovlivněn. To znamená, že z třídy unikají informace {A} do třídy {A, B}, což je porušení zásady důvěrnosti. Tento únik by měl být detekován systémem typu zabezpečení.

Příklad

Návrh systému typu zabezpečení vyžaduje funkci (označovanou také jako prostředí zabezpečení), která vytváří mapování z proměnných na typy zabezpečení nebo třídy. Tuto funkci lze nazvat Γ, takovou Γ (x) = τ, kde X je proměnná a τ je třída zabezpečení nebo typ. Třídy zabezpečení se přiřazují (také nazývají „úsudek“) komponentám programu pomocí následující notace:

• K operacím čtení jsou přiřazeny typy: ⊢ ⊢ e: τ.
• K operacím zápisu jsou přiřazeny typy: Γ ⊢ S: τ cmd.
• Konstantám lze přiřadit libovolný typ.

K dekompozici programu lze použít následující zápis zdola nahoru: předpoklad₁ ... předpoklad_n/závěr. Jakmile je program rozložen na triviální soudy, pomocí kterých lze snadno určit typ, typy pro méně triviální části programu mohou být vyčerpány. Každý „čitatel“ je považován za izolovaný, přičemž se dívá na typ každého příkazu, aby zjistil, zda lze pro „jmenovatele“ odvodit povolený typ na základě „pravidel“ systému definovaného typu.

Pravidla

Hlavní částí systému typu zabezpečení jsou pravidla. Říkají, jak by měl být program rozložen a jak by mělo být provedeno ověření typu. Tento program hračky se skládá z podmíněného testu a dvou možných přiřazení proměnných. Pravidla pro tyto dvě události jsou definována takto:

Použitím tohoto jednoduchého programu zavedeného výše získáte:

Typový systém detekuje porušení zásad na řádku 2, kde je operace čtení bezpečnostní třídy {A} provádí se, následují dvě operace zápisu méně přísné třídy zabezpečení {A, B}. Formálněji řečeno, {A} ⋢ {A, B}, {A, B} (z pravidla podmíněného testu). Program je tedy klasifikován jako „nepopsatelný“.

Zdravost

Zvuk systému typu zabezpečení lze neformálně definovat jako: If program P je dobře napsaný, P uspokojuje nezasahování.

Reference

Další čtení

• Fred B. Schneider, Greg Morrisett a Robert Harper, Jazykový přístup k zabezpečení.
• Andrei Sabelfeld, Andrew C. Myers, Jazykové zabezpečení toku informací.