Przepływ informacji (teoria informacji) - Information flow (information theory)

Przepływ informacji w informacyjnym kontekście teoretycznym to transfer informacji ze zmiennej do zmiennej w danym procesie . Nie wszystkie przepływy mogą być pożądane; na przykład system nie powinien ujawniać żadnych tajemnic (częściowo lub nie) do publicznych obserwatorów. ${\ displaystyle x}$ ${\ displaystyle y}$

Wprowadzenie

Zabezpieczenie danych manipulowanych przez systemy komputerowe było wyzwaniem w ostatnich latach. Obecnie istnieje kilka metod ograniczania ujawniania informacji, takich jak listy kontroli dostępu , zapory sieciowe i kryptografia . Jednakże, chociaż metody te nakładają ograniczenia na informacje, które są udostępniane przez system, nie zapewniają one żadnej gwarancji propagacji informacji . Na przykład listy kontroli dostępu systemów plików zapobiegają nieautoryzowanemu dostępowi do plików, ale nie kontrolują sposobu późniejszego wykorzystania danych. Podobnie kryptografia zapewnia środki do prywatnej wymiany informacji za pośrednictwem niezabezpieczonego kanału, ale po ich odszyfrowaniu nie daje się żadnych gwarancji dotyczących poufności danych.

W niskopoziomowej analizie przepływu informacji każdej zmiennej przypisany jest zwykle poziom bezpieczeństwa. Podstawowy model składa się z dwóch różnych poziomów: niskiego i wysokiego, co oznacza odpowiednio informację publicznie obserwowalną i informację tajną. Aby zapewnić poufność, nie należy zezwalać na przepływ informacji od wysokich do niskich zmiennych. Z drugiej strony, aby zapewnić integralność, należy ograniczyć przepływy do wysokich zmiennych.

Bardziej ogólnie, poziomy bezpieczeństwa można postrzegać jako kratownicę, w której informacje przepływają tylko w górę w sieci.

Na przykład, biorąc pod uwagę dwa poziomy bezpieczeństwa i (niski i wysoki), jeżeli przepływy z do , z do i do byłyby dozwolone, natomiast przepływy z do nie. ${\ displaystyle L}$ ${\ displaystyle H}$ ${\ displaystyle L \ leq H}$ ${\ displaystyle L}$ ${\ displaystyle L}$ ${\ displaystyle H}$ ${\ displaystyle H}$ ${\ displaystyle L}$ ${\ displaystyle H}$ ${\ displaystyle H}$ ${\ displaystyle L}$

W całym artykule używany jest następujący zapis:

zmienna (niska) oznacza zmienną obserwowalną publicznie ${\ displaystyle l \ in L}$
zmienna (wysoka) oznacza tajną zmienną ${\ displaystyle h \ in H}$

Gdzie i są jedynymi rozważanymi poziomami bezpieczeństwa w kratownicy . ${\ displaystyle L}$ ${\ displaystyle H}$

Jawne przepływy i kanały boczne

Przepływy informacji można podzielić na dwie główne kategorie. Najprostszym z nich jest jawny przepływ, w którym pewien sekret jawnie wycieka do publicznie obserwowalnej zmiennej. W poniższym przykładzie sekret w zmiennej h wpływa do publicznie obserwowalnej zmiennej l .

var l, h
l := h

Pozostałe przepływy należą do kategorii kanałów bocznych . Na przykład w ataku czasowym lub ataku z analizą mocy system przecieka informacje odpowiednio przez czas lub moc potrzebną do wykonania akcji w zależności od wartości tajnej.

W poniższym przykładzie osoba atakująca może wywnioskować, czy wartość h wynosi jeden, czy nie, do czasu zakończenia programu:

var l, h
if h = 1 then
    (* do some time-consuming work *)
l := 0

Kolejnym przepływem w kanale bocznym jest niejawny przepływ informacji, który polega na wycieku informacji przez przepływ sterowania programem. Poniższy program (niejawnie) ujawnia wartość tajnej zmiennej h zmiennej l . W tym przypadku, ponieważ zmienna h jest logiczna, wszystkie bity zmiennej h są ujawniane (na końcu programu l będzie równe 3, jeśli h jest prawdziwe, a 42 w przeciwnym razie).

var l, h
if h = true then
    l := 3
else
    l := 42

Brak zakłóceń

Nieingerencja to polityka, która wymusza, aby osoba atakująca nie była w stanie odróżnić dwóch obliczeń od ich wyników, jeśli różnią się jedynie tajnymi danymi wejściowymi. Jednak ta polityka jest zbyt rygorystyczna, aby mogła być stosowana w realistycznych programach. Klasycznym przykładem jest program do sprawdzania haseł, który, aby był użyteczny, musi ujawnić pewne tajne informacje: czy hasło wejściowe jest poprawne, czy nie (zwróć uwagę, że informacje, które napastnik poznaje w przypadku, gdy program odrzuci hasło, to próbowane hasło nie jest poprawne).

Kontrola przepływu informacji

Mechanizm kontroli przepływu informacji to taki, który wymusza zasady przepływu informacji. Zaproponowano kilka metod egzekwowania polityki przepływu informacji. Mechanizmy wykonawcze oznaczające dane etykietami przepływu informacji zostały zastosowane na poziomie systemu operacyjnego i na poziomie języka programowania. Opracowano również statyczne analizy programów, które zapewniają zgodność przepływu informacji w ramach programów z polityką.

Opracowano analizę statyczną i dynamiczną dla obecnych języków programowania. Jednak techniki analizy dynamicznej nie mogą obserwować wszystkich ścieżek wykonania, a zatem nie mogą być jednocześnie solidne i precyzyjne. Aby zagwarantować brak zakłóceń, albo przerywają wykonania, które mogą ujawnić poufne informacje, albo ignorują aktualizacje, które mogą wyciekać informacje.

Ważnym sposobem egzekwowania zasad przepływu informacji w programie jest zastosowanie systemu typów zabezpieczeń, czyli systemu typów, który wymusza właściwości zabezpieczeń. W takim solidnym systemie typu, jeśli program sprawdza typ, spełnia on zasady przepływu i dlatego nie zawiera niewłaściwych przepływów informacji.

System typu zabezpieczenia

W języku programowania rozszerzonym o system typów zabezpieczeń każde wyrażenie zawiera zarówno typ (np. Logiczną lub całkowitą), jak i etykietę bezpieczeństwa.

Poniżej znajduje się prosty system zabezpieczeń, który wymusza brak zakłóceń. Notacja oznacza, że wyrażenie ma typ . Podobnie oznacza, że polecenie jest możliwe do wpisania w kontekście zabezpieczeń . ${\ Displaystyle \; \ vdash exp \;: \; \ tau}$ ${\ displaystyle exp}$ ${\ Displaystyle \; \ tau}$ ${\ displaystyle [sc] \ vdash C}$ ${\ displaystyle C}$ ${\ displaystyle sc}$

${\ displaystyle [E1-2] \ quad \ vdash exp: wysoki \ qquad {\ frac {h \ notin Vars (exp)} {\ vdash exp \;: \; niski}}}$

${\ Displaystyle [C1-3] \ quad [sc] \ vdash {\ textbf {pomiń}} \ qquad [sc] \ vdash h \;: = \; exp \ qquad {\ frac {\ vdash exp \;: \ ; low} {[low] \ vdash l \;: = \; exp}}}$

${\ Displaystyle [C4-5] \ quad {\ Frac {[sc] \ vdash C_ {1} \ quad [sc] \ vdash C_ {2}} {[sc] \ vdash C_ {1} \ ;; \; C_ {2}}} \ qquad {\ frac {\ vdash exp \;: \; sc \ quad [sc] \ vdash C} {[sc] \ vdash {\ textbf {while}} \ exp \ {\ textbf { do}} \ C}}}$

${\ Displaystyle [C6-7] \ quad {\ Frac {\ vdash exp \;: \; sc \ quad [sc] \ vdash C_ {1} \ quad [sc] \ vdash C_ {2}} {[sc] \ vdash {\ textbf {if}} \ exp \ {\ textbf {then}} \ C_ {1} \ {\ textbf {else}} \ C_ {2}}} \ qquad {\ frac {[high] \ vdash C} {[low] \ vdash C}}}$

Dobrze wpisane polecenia obejmują na przykład

{\ Displaystyle [niski] \ vdash \ {\ textbf {if}} \ l = 42 \ {\ textbf {wtedy}} \ h \;: = \; 3 \ {\ textbf {else}} \ l \ ;: = \; 0}

.

I odwrotnie, program

{\ Displaystyle l \;: = \; 0 \; \ {\ textbf {a}} \ l <h \ {\ textbf {do}} \ l \;: = \; l + 1}

jest źle wpisany, ponieważ ujawni wartość zmiennej w . ${\ displaystyle h}$ ${\ displaystyle l}$

Zauważ, że reguła jest regułą subsumpcji, co oznacza, że może nią być dowolne polecenie typu bezpieczeństwa . Na przykład może to być zarówno i . Nazywa się to polimorfizmem w teorii typów . Podobnie, rodzaj wyrażenia , że spełnia może być jednocześnie oraz zgodnie z i odpowiednio. ${\ displaystyle [C7]}$ ${\ displaystyle high}$ ${\ displaystyle low}$ ${\ displaystyle h: = 1}$ ${\ displaystyle high}$ ${\ displaystyle low}$ ${\ displaystyle exp}$ ${\ displaystyle h \ notin Vars (exp)}$ ${\ displaystyle high}$ ${\ displaystyle low}$ ${\ displaystyle [E1]}$ ${\ displaystyle [E2]}$

Odtajnienie

Jak pokazano wcześniej, polityka braku zakłóceń jest zbyt rygorystyczna, aby można ją było stosować w większości rzeczywistych aplikacji. Dlatego opracowano kilka podejść, aby umożliwić kontrolowane ujawnianie informacji. Takie podejścia nazywane są odtajnianiem informacji.

Solidna odtajnianie wymaga, aby aktywny napastnik nie mógł manipulować systemem, aby poznać więcej sekretów niż to, co już wiedzą pasywni atakujący.

Konstrukcje odtajniania informacji można sklasyfikować w czterech ortogonalnych wymiarach: jakie informacje są ujawniane, kto jest upoważniony do dostępu do informacji, gdzie informacje są ujawniane i kiedy są ujawniane.

Co

Co kontrole, które informacje (częściowe lub nie) polityczne odtajnienie mogą być uwalniane do zmiennej publicznie widoczne.

Poniższy przykład kodu przedstawia konstrukcję odtajniania z. W tym kodzie wartość zmiennej h jest jawnie dozwolona przez programistę do wpłynięcia do publicznie obserwowalnej zmiennej l .

var l, h
if l = 1 then
    l := declassify(h)

WHO

Który kontroluje polityki odtajnienie których dyrektorzy (czyli kto) może uzyskać dostęp do danej informacji. Taka polityka została zaimplementowana w kompilatorze Jif.

Poniższy przykład pozwala Bobowi udostępnić Alicji swój sekret zawarty w zmiennej b za pośrednictwem powszechnie dostępnej zmiennej ab .

var ab                                (* {Alice, Bob} *)
var b                                 (* {Bob} *)
if ab = 1 then
    ab := declassify(b, {Alice, Bob}) (* {Alice, Bob} *)

Gdzie

A gdzie polityka odtajniania reguluje, gdzie informacje mogą zostać udostępnione, na przykład poprzez kontrolowanie, w których wierszach informacji kodu źródłowego mogą zostać udostępnione.

Poniższy przykład wykorzystuje konstrukcję przepływu zaproponowaną w. Ta konstrukcja przyjmuje strategię przepływu (w tym przypadku zmienne w H mogą przepływać do zmiennych w L) i polecenie, które jest uruchamiane w ramach danej strategii przepływu.

var l, h
flow H  $\prec$  L in
    l := h

Gdy

A kiedy polityka odtajniania reguluje, kiedy informacje mogą zostać ujawnione. Polityki tego rodzaju można wykorzystać do weryfikacji programów realizujących np. Kontrolowane ujawnianie tajnych informacji po dokonaniu płatności lub zaszyfrowanych tajemnic, które nie powinny być ujawniane w określonym czasie przy wielomianowej mocy obliczeniowej.

Metody odtajniania dla przepływów niejawnych

Niejawny przepływ występuje, gdy kod, którego warunkowe wykonanie jest oparte na prywatnych informacjach, aktualizuje zmienną publiczną. Jest to szczególnie problematyczne, gdy rozważa się wielokrotne wykonanie, ponieważ osoba atakująca może wykorzystać zmienną publiczną do wywnioskowania informacji prywatnych, obserwując, jak zmienia się jej wartość w czasie lub wraz z danymi wejściowymi.

Naiwne podejście

Naiwne podejście polega na egzekwowaniu własności poufności wszystkich zmiennych, na których wartość wpływają inne zmienne. Ta metoda prowadzi do częściowego wycieku informacji, ponieważ w niektórych wystąpieniach aplikacji zmienna ma wartość Niska, a w innych Wysoka.

Brak wrażliwej aktualizacji

Żadna wrażliwa aktualizacja nie zatrzymuje programu, gdy zmienna High wpływa na wartość zmiennej Low, skutecznie zapobiegając wyciekowi informacji. Ponieważ po prostu wyszukuje wyrażenia, w których wyciek informacji może nastąpić bez patrzenia na kontekst, może zatrzymać program, który pomimo potencjalnego wycieku informacji nigdy nie wycieka informacji.

W poniższym przykładzie x jest wysokie, a y to niskie.

var x, y
y := false
if h = true then
    y := true
return true

W tym przypadku program zostałby zatrzymany, ponieważ używa wartości zmiennej High do zmiany zmiennej Low, mimo że program nigdy nie wycieka informacji.

Dopuszczalne ulepszenie

Permissive-upgrade wprowadza dodatkową klasę bezpieczeństwa P, która będzie identyfikować zmienne wycieku informacji. Kiedy zmienna High wpływa na wartość zmiennej Low, ta ostatnia jest oznaczona jako P. Jeżeli zmienna z etykietą P wpływa na zmienną Low, program zostanie zatrzymany. Aby zapobiec zatrzymaniu, zmienne Niska i P należy przekształcić na Wysokie przy użyciu funkcji prywatyzacji, aby zapobiec wyciekowi informacji. W kolejnych przypadkach program będzie działał bez przerwy.

Wnioskowanie prywatyzacyjne

Wnioskowanie o prywatyzacji rozszerza zezwolenie na aktualizację, aby automatycznie zastosować funkcję prywatyzacji do każdej zmiennej, która może spowodować wyciek informacji. Ta metoda powinna być używana podczas testowania, gdzie konwertuje większość zmiennych. Gdy program wejdzie do produkcji, należy zastosować zezwolenie na aktualizację, aby zatrzymać program w przypadku wycieku informacji, a funkcje prywatyzacyjne można zaktualizować, aby zapobiec kolejnym wyciekom.

Zastosowanie w systemach komputerowych

Oprócz aplikacji do języka programowania, teorie kontroli przepływu informacji zostały zastosowane w systemach operacyjnych, systemach rozproszonych i przetwarzaniu w chmurze.

Languages

In other projects