2
Políticas, Modelos e Mecanismos de
Segurança
 O papel do controle de acesso
 Matriz de controle de acesso
 Resultados fundamentais
 Políticas de segurança
 Modelos de segurança
 Mecanismos e implementação
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
1
Resultados fundamentais (1)
 Questões fundamentais
• Como se pode determinar que um sistema é seguro?
– Qual é a definição de “sistema seguro”?
• Existe um algoritmo genérico que permite determinar se um sistema é
seguro?
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
2
Resultados fundamentais (2)
 Definição de sistema seguro (1)
•
Definição simples
– É aquele que não permite a violação da política de segurança
• Definição adotada por (HARRISON et al., 1976) (1)
– Política baseada na distribuição de direitos para sujeitos
 Seja R o conjunto de direitos genéricos (primitivos) do sistema
 Quando um direito genérico r é adicionado a um elemento da matriz de controle de
acesso que ainda não contém r, diz-se que ocorreu o vazamento do direito r
– Isto é, a política define o conjunto de estados autorizados A como sendo o
conjunto de estados para o qual nenhum comando c(x1, ..., xn) pode vazar o
direito r
 Não há distinção entre vazamento de direitos e transferência autorizada de direitos
(C) 2005 Gustavo Motta
 Não há sujeitos confiáveis
©2002-2004 Matt Bishop
3
Resultados fundamentais (3)
 Definição de sistema seguro (2)
• Definição adotada por (HARRISON et al., 1976) (2)
– Seja um sistema de computação num estado de proteção inicial S0
– O sistema é seguro (safe) com respeito ao direito r se r jamais puder ser
vazado. Caso o sistema possa vazar o direito r (entrar num estado não
autorizado), diz-se que o sistema é inseguro (unsafe) com respeito ao direito r
• Distinção entre safe e secure
– Safe refere-se a um modelo abstrato
– Secure refere-se a uma implementação real do modelo
– Um sistema secure corresponde a um modelo safe com respeito a todos os
direitos, enquanto um modelo safe com respeito a todos os direitos não garante
um sistema secure
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
4
Resultados fundamentais (4)
 Safety question
• Sejam
– O estado inicial X0 = (S0, O0, A0)
– Um conjunto de comandos C
– r  A0[s, o], r  R, s  S0, o  O0
• Existe um algoritmo para determinar que um estado Xn pode ser alcançado,
onde
–  s, o tal que r  An[s, o] e r  A0[s, o] ?
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
5
Resultados fundamentais (5)
 Teorema: Existe um algoritmo que determina (decide) se um dado
sistema de proteção mono-operacional com estado inicial S0 é
seguro (safe) com respeito a um direito genérico r (HARRISON et
al., 1976)
• Esquema da prova (1):
– Considerar a seqüência mínima de comandos c1, ..., ck para vazar r
– Pode-se omitir os comandos delete e destroy: não podem vazar ou serem
detectados, pois não se pode testar a ausência de direitos na MCA
– Pode-se fundir todos comandos create em apenas um: nenhum comando monooperacional pode, isoladamente, criar um objeto/sujeito e entrar com direitos, logo
múltiplas criações podem ser removidas, deixando-se a criação de um único sujeito
 Não há teste para ausência de direitos
 Testes em A[s1, o1] e em A[s2, o2] têm o mesmo resultado que os mesmos testes em
Motta
6
A[s1, o1] e em A[s1, o2(C)
] = 2005
A[s1,Gustavo
o2] A[s
2, o2]
©2002-2004 Matt Bishop
Resultados fundamentais (6)
• Esquema da prova (2):
– Caso n direitos possam ser vazados, então n(|S0| + 1)(|O0| + 1) comandos são
necessários para entrar com cada direito em cada elemento da matriz
– No pior caso, um novo sujeito é criado, então, lembrando que c1, ..., ck é a
seqüência mínima de comandos para vazar r, tem-se que
 k  n(|S0| + 1)(|O0| + 1) + 1
– Isto é, no pior caso, o tamanho da computação que pode levar a um vazamento é
limitada a k
• Pela enumeração de todos os estados possíveis, pode-se determinar se um
sistema de proteção mono-operacional é safe
– Tentar todas as seqüências de comandos enter, opcionalmente começando pelo
comando create subject,(C)
com
tamanhos
limitados a k
2005
Gustavo Motta
©2002-2004 Matt Bishop
7
Resultados fundamentais (7)
 Infelizmente, o resultado anterior não se generaliza para todos os
sistemas de proteção
• Ou seja, a resposta à Safety Question é não, para sistemas de proteção em
geral
 Teorema: Não é decidível se um dado estado de um dado sistema de
proteção é seguro (safe) para um dado direito genérico (HARRISON
et al., 1976)
• Esquema da prova (1)
– Prova por contradição
 Mostra-se que uma máquina de Turing arbitrária pode ser reduzida à Safety Question,
com a máquina de Turing entrando num estado final correspondente ao vazamento de
um dado direito genérico
 Então, caso a Safety Question seja decidível, pode-se determinar quando a máquina de
Turing pára, mostrando
problema
da parada é decidível, o que não é verdadeiro,
(C)que
2005o Gustavo
Motta
8
Matt Bishop
logo, conclui-se que a©2002-2004
Safety Question
é não decidível
Resultados fundamentais (8)
• Esquema da prova (2)
– Revisão de máquinas de Turing
 Fita infinita numa direção
 Estados K, símbolos M e um valor distinto para branco b
 Função de transição (k, m) = (k, m, L) significando que no estado k, o símbolo m
numa posição da fita é alterada para o símbolo m, com a cabeça da máquina movendose uma posição à esquerda (direita se R). Depois, a máquina entra no estado k
 A máquina de Turing pára quando entra no estado qf
fita
1
2
A
B C
3
4
D …
cabeça
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
O estado corrente é k
O símbolo corrente é C
9
Resultados fundamentais (9)
• Esquema da prova (2)
– Mapeamento de uma máquinas de Turing para um sistema de proteção
 Símbolos e estados
 direitos, porém diferenciados
 Células da fita
 sujeitos
 Célula si contém A
 si possui o direito A sobre si mesmo
 Célula sk (mais a direita)
 sk possui o direito end sobre si mesmo
 Máquina no estado p e cabeça
 si possui o direito p sobre si mesmo
na célula si
 Direito diferenciado own
» si possui o direito own sobre si+1, para 1  i < k
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
10
Resultados fundamentais (10)
• Esquema da prova (3)
– Mapeamento de uma máquinas de Turing para um sistema de proteção
1
2
A
B C D …
3
4
s1
cabeça
s1
s2
A
own
s2
O estado corrente é k
s3
s4
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
B
s3
s4
own
Ck
own
D end
11
Resultados fundamentais (11)
• Esquema da prova (4)
– Mapeamento de uma máquinas de Turing para um sistema de proteção
1
2
A
B X D …
3
4
s1
cabeça
s1
s2
A
own
s2
Após (k, C) = (k1, X, R),
onde k estado corrente e
k1 é o próximo estado
s3
s4
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
B
s3
s4
own
X
own
D k1 end
12
Resultados fundamentais (12)
• Esquema da prova (5)
(4)
– Mapeamento de uma máquinas de Turing para um sistema de proteção
(k, C) = (k1, X, R), numa célula diferente da mais à direita, é mapeada pelo
comando
command ck, C(si3,, ssi+1
4) )
if own in a[si3,, ssi+1
andkkinina[s
a[s3,i,ss3i]] and
and C
C in
in a[s
a[s3i, si3]]
4] ]and
then
delete k from a[si3,, ssi3];];
delete C from a[si3,, ssi3];];
enter X into a[si3,, ssi3];];
enter k1 into a[si+1
, 4s];i+1];
4, s
end
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
13
Resultados fundamentais (13)
• Esquema da prova (6)
– Mapeamento de uma máquinas de Turing para um sistema de proteção
1
2
A
B C D …
3
4
s1
cabeça
s1
s2
A
own
s2
O estado corrente é k
s3
s4
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
B
s3
s4
own
Ck
own
D end
14
Resultados fundamentais (14)
• Esquema da prova (5)
– Mapeamento de uma máquinas de Turing para um sistema de proteção
1
2
A
B X D …
3
4
s1
cabeça
s1
s2
A
own
s2
Após (k, C) = (k1, X, L),
onde k estado corrente e
k1 é o próximo estado
s3
s4
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
s3
s4
B k1 own
X
own
D end
15
Resultados fundamentais (15)
• Esquema da prova (6)
(4)
– Mapeamento de uma máquinas de Turing para um sistema de proteção
(k, C) = (k1, X, L), numa célula, é mapeada pelo comando
command ck, C(si3,, ssi1
2) )
if own in a[si1
andkkinina[s
a[s3,i,ss3i]] and
and C
C in
in a[s
a[s3i, s3i]]
2, s, 3s]i]and
then
delete k from a[si3,, ssi3];];
delete C from a[si3,, ssi3];];
enter X into a[si3,, ssi3];];
enter k1 into a[si1
2, s, 2s];
i1];
end
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
16
Resultados fundamentais (16)
• Esquema da prova (7)
– Mapeamento de uma máquinas de Turing para um sistema de proteção
1
2
A
B X D …
3
4
s1
cabeça
O estado corrente é k1
s1
s2
A
own
s2
s3
s4
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
B
s3
s4
own
X
own
D k1 end
17
Resultados fundamentais (17)
• Esquema da prova (8)
– Mapeamento de uma máquinas de Turing para um sistema de proteção
1
2
A
B X Y
3
4
5
…
s1
cabeça
s1
s2
A
own
s2
Após (k1, D) = (k2, Y, R),
onde k1 é o estado corrente
e k2 próximo estado
s3
s4
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
B
s3
s4
s5
own
X
own
Y
own
b k2 end
18
Resultados fundamentais (18)
• Esquema da prova (9)
– Mapeamento de uma máquinas de Turing para um sistema de proteção
(k1, D) = (k2, Y, R), na célula mais à direita, é mapeada pelo comando
command crightmostk,C(si4,, ssi+1
5) )
if end in A[si4,, ssi4]]and
andkk11in
inA[s
A[si,4,sis]4and
] andDDininA[s
A[s
i, 4s,i]s4]
then
delete end from A[si4,, ssi4];];
create subject si+1
5; ;
enter own into A[si4,, ssi+1
5];];
enter end into A[si+1
, 5s];i+1];
5, s
enter b into A[si+1
5, s, 5s];
i+1];
delete k1 from A[si4,, ssi4];];
delete D from A[si4,, ssi4];];
enter Y into A[si4,, ssi4];];
enter k2 into A[si+1
, 5s];i+1];
5, s
end
©2002-2004 Matt Bishop
Resultados fundamentais (19)
• Esquema da prova (10)
– Restante da prova
 O sistema de proteção simula exatamente uma máquina de Turing
» Exatamente 1 direito end na MCA
» 1 dos direitos das células corresponde ao estado da máquina de Turing
» Logo, no máximo, um comando é aplicável por vez
 Caso a máquina de Turing entre no estado qf, então houve vazamento de direitos
 Caso a Safety Question seja decidível, então representa-se uma máquina de Turing como
visto e determina-se se qf vaza
» O que implica que o problema da parada é decidível – falsidade
 Conclusão: a Safety Question
não decidível
(C) 2005é Gustavo
Motta
©2002-2004 Matt Bishop
20
Resultados fundamentais (20)
 Outros resultados
• O conjunto dos sistemas proteção unsafe é recursivamente enumerável
– Pode-se gerar a lista de todos os sistemas unsafe
– Pode ser reconhecido por uma máquina de Turing
• Excluíndo-se as primitivas create, então a safety question pode ser completada
em P-SPACE
• Excluíndo-se as apenas as primitivas delete e destroy, a safety question é não
decidível
– Os sistemas são monotônicos
• A safety question para sistemas monotônicos e bicondicionais não é decidível
• A safety question para sistemas monotônicos e monocodicionais é decidível
• A safety question para sistemas monocodicionais com create, enter e delete,
mas sem destroy) é decidível
(C) 2005 Gustavo Motta
21
©2002-2004 Matt Bishop
Resultados fundamentais (21)
 Conclusões
• Safety não é decidível em modelos de proteção genéricos, mas pode-se tornar
decidível se o sistema de proteção for restringido de um modo particular
• A atenção volta-se à concepção de modelos de controle de acesso para os quais
a safety question é decidível, em vez de se desenvolver uma teoria geral de
sistemas seguros
– Restrição no uso dos direitos take e grant
– Restrição da delegação
 Questões
• Dado um sistema particular, com regras de transformação específicas, pode-se
mostrar que a safety question é decidível?
• Quais são as restrições mais fracas num sistema de proteção que tornam a
safety question decidível nesse sistema?
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
22
Resultados fundamentais (22)
 Modelo de proteção take-grant (1)
• Sistema específico, com um conjunto de regras para transição de estados
– Take
– Grant
– Create
– Remove
• Safety é decidível em tempo linearmente proporcional ao tamanho do sistema
– O(|V| + |E|)
• Objetivo
– Encontrar as condições, sob as quais, direitos podem ser transferidos de uma
entidade para outra no sistema
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
23
Resultados fundamentais (23)
 Modelo de proteção take-grant (2)
• O sistema é representado por um grafo direcionado
– Sujeito:
– Objeto:
Sujeito ou objeto:
– O segmento rotulado indica os direitos um vértice de origem tem sobre um vértice de destino
• Regra take – α  β
α
β
t
x
z
y
β
t
├
x
z
y
x takes (α para y) de z
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
24
Resultados fundamentais (24)
 Modelo de proteção take-grant (3)
• Regra grant – α  β
β
g
x
α
z
y
β
g
├
z
x
y
z grants (α para y) para x
• Regra create – α  R
α
├
x
y
x creates (α para o novo vértice) y
• Regra remove – α  β
β
β -α
├
x
y
x
x
(C) 2005 Gustavo Motta
©2002-2004(α
Matt
removes
to)Bishop
y
y
25
Resultados fundamentais (25)
 Modelo de proteção take-grant (4)
• Compartilhamento de direitos
– Dado G0, um vértice x pode obter direitos α sobre y?
 Can_share(α, x, y, G0) é verdade se e somente se
» G0├* Gn usando apenas as 4 regras, e
» Existe um segmento α de x para y em Gn
– tg-path: é a seqüência de vértices v0,…,vn não vazia, com segmentos t ou g entre
quaisquer pares de vértices vi, vi+1
 Vértices são tg-connected se existe um tg-path entre eles
– Teorema: quaisquer dois sujeitos com tg-path de tamanho 1 podem compartilhar
direitos
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
26
Resultados fundamentais (26)
 Modelo de proteção take-grant (5)
• Compartilhamento de direitos
– Teorema: quaisquer dois sujeitos com tg-path de tamanho 1 podem compartilhar
direitos - Can_share(α, x, y, G0)
– Esquema da prova:
x
z
y
 1. Regra take
t
βα
 2. Regra grant
g
βα
 3. Lema 3.1
t
βα
(C) 2005 Gustavo Mottag
©2002-2004 Matt Bishop
βα
 4. Lema 3.2
27
Resultados fundamentais (27)
 Modelo de proteção take-grant (5)
• Compartilhamento de direitos
– Teorema: quaisquer dois sujeitos com tg-path de tamanho 1 podem compartilhar
direitos - Can_share(α, x, y, G0)
– Esquema da prova:
 Lema 3.1
βα
t
x
α
z
├*
y
βα
t
tg
g
α
 Lema 3.2 – resultado similar
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
28
Resultados fundamentais (28)
 Modelo de proteção take-grant (5)
• Ilha: máximo subgrafo composto apenas com sujeitos tg-connected
– Quaisquer direitos possuídos por um vértice qualquer numa ilha podem ser
compartilhados com qualquer outro vértice da ilha
 Prova: indução sobre o teorema anterior
• Ponte: é um tg-path entre os pontos finais v0 e vn, ambos sujeitos, com
segmentos da seguinte forma
– t→*
– t←*
– t→* g→ t←*
– t→* g← t←*
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
29
Resultados fundamentais (29)
 Modelo de proteção take-grant (6)
• Ponte: é um tg-path entre os pontos finais v0 e vn, ambos sujeitos, com
segmentos da seguinte forma
– Exemplo
t
g
t
v0
vn
t
g
t
v0
vn
α
1. Pelo lemma 3.1
α
α
2. Por grant
3. Por take
α
t
v0
g
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
t
?
vn
30
Resultados fundamentais (30)
 Modelo de proteção take-grant (6)
• Teorema: o predicado Subject_can_share(α, x, y, G0) é verdadeiro, se e
somente se, x e y são sujeitos e existe um segmento α de x para y em G0 OU
se:
–  um sujeito s  G0 com um segmento s-to-y rotulado com α, e
–  ilhas I1, …, In tal que x  I1, s  In, e existe uma ponte de Ij para Ij+1
(1  j  n)
x
I1
s
α
α
I2
α
α
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
y
In
31
Resultados fundamentais (31)
 Modelo de proteção take-grant (7)
• Generalização para incluir objetos – definições auxiliares
– x initially spans para y se x é um sujeito e existe um tg-path com uma palavra associada em
{t→*g→}  {} entre eles
 x pode conceder um direito para y
– x terminally spans para y se x é um sujeito e existe um tg-path com uma palavra associada
em {t→*}  {} entre eles
 x pode pegar um direito de y
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
32
Resultados fundamentais (32)
 Modelo de proteção take-grant (8)
• Teorema: o predicado Can_share(α, x, y, G0) é verdadeiro, se e somente se,
existe um segmento α de x para y em G0 OU se:
–  um vértice s  G0 com um segmento s-to-y rotulado com α
–  um sujeito x’, tal que, x’=x ou x’ initially spans para x,
–  um sujeito s’ , tal que, s’=s ou s’ terminally spans para s, e
–  ilhas I1, …, In tal que x’  I1, s’  In, e existe uma ponte de Ij para Ij+1
(1  j  n)
x’
s’
I1
α
I2
α
x
x’ pode conceder um direito a x
(C) 2005 Gustavo α
Motta
©2002-2004 Matt Bishop
In
s
α
y
s’ pode tomar um direito
33 de s
Resultados fundamentais (33)
 Modelo de proteção take-grant (9)
• Corolário: existe um algoritmo com complexidade O(|V| + |E|) que testa o
predicado Can_share, no qual, V é o conjunto de vértices e E é o conjunto de
segmentos em G0
– A Safety Question é decidível em tempo linear
• O compartilhamento de direitos requer a cooperação de todos sujeitos
envolvidos
– Roubo e Conspiração
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
34
Resultados fundamentais (34)
 Questões chave
• Dado que se pode responder à safety question em sistemas específicos, por que
não se pode respondê-la para sistemas genéricos?
• Quais características distinguem um modelo no qual a safety question é
decidível daqueles em que essa questão não é decidível?
 Avanços
• Modelo de proteção esquemático (SPM)
• Modelo de proteção esquemático estendido (ESPM)
• Modelo de matriz de acesso tipado (TAM)
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
35
Resultados fundamentais (35)
 Modelo de proteção esquemático (SPM)
• Baseia-se na noção de um tipo de proteção
– Rótulo que determina como os direitos de controle afetam uma entidade
• Direitos são particionados nos conjuntos
– Direitos inertes (DI)
 Não alteram o estado de proteção do sistema
» Por exemplo, ler um arquivo não altera quais entidades podem acessar esse documento, logo o
direito ler é um DI
– Direitos de controle (DC)
 Altera o estado de proteção do sistema
» A aplicação da regra take no modelo take-grant altera o estado de proteção do sistema, logo o
(C) 2005
36
direito take é um direito
DC Gustavo Motta
©2002-2004 Matt Bishop
Resultados fundamentais (36)
 Modelo de proteção esquemático estendido (ESPM)
• O SPM assume implicitamente a noção de um único ancestral
• ESPM permite a existência de mais de um ancestral
– Problema que surge em sistemas distribuídos
• Exemplo
– Ana e João devem cooperar para realizar uma certa tarefa, mas um não confia no
outro
 Solução baseada na criação de um proxy em conjunto
» Cada um concede ao proxy apenas aqules direitos necessários à realização da tarefa
» É proibido às partes(C)
copiar
doMotta
proxy
2005direitos
Gustavo
©2002-2004 Matt Bishop
37
Resultados fundamentais (37)
 Modelo de matriz de acesso tipado (TAM)
• As propriedades de safety dos modelos SPM e ESPM são baseadas na noção
de “tipos”
– O modelo TAM introduz a noção de tipos explicitamente e possui propriedades
safety similares às dos modelos SPM e ESPM
• O tipo de uma entidade é fixado quando ela é criada (ou no estado inicial) e ele
permanece fixo ao longo da vida do modelo
• O estado de proteção de um sistema é (S, O, , A), onde S é o conjunto de
sujeitos, O é o conjunto de objetos, A é a MCA e : O  T é uma função de
tipo, que especifica o tipo de
cada objeto
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
38
Resultados fundamentais (38)
 Conclusão
• A safety question é um problema rico que trouxe o desenvolvimento de vários
modelos e técnicas de análise
– Tais modelos oferecem insights para o limiar entre decidibilidade e não
decidibilidade – tipos são importantes para análise da safety question
– Do ponto de vista da security, ajuda no entendimento de quando a análise da
segurança é tratável e quando não é
• Saber qual o conjunto de características suficientes e necessárias para tornar o
safety question um problema
decidível ainda é uma questão em aberto
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
39
Referências (1)

HARRISON, M.; RUZZZO, W. e ULLMAN, J. Protection in operating systems.
Communications of the ACM, v. 19, n. 8, p. 461-471, 1976.
(C) 2005 Gustavo Motta
©2002-2004 Matt Bishop
40