Curso MIT "Segurança de sistemas de computadores". Palestra 10: Execução Simbólica, Parte 1

Instituto de Tecnologia de Massachusetts. Curso de Aula nº 6.858. "Segurança de sistemas de computador". Nikolai Zeldovich, James Mickens. 2014 ano

Computer Systems Security é um curso sobre o desenvolvimento e implementação de sistemas de computador seguros. As palestras abrangem modelos de ameaças, ataques que comprometem a segurança e técnicas de segurança baseadas em trabalhos científicos recentes. Os tópicos incluem segurança do sistema operacional (SO), recursos, gerenciamento de fluxo de informações, segurança de idiomas, protocolos de rede, segurança de hardware e segurança de aplicativos da web.

Palestra 1: “Introdução: modelos de ameaças” Parte 1 / Parte 2 / Parte 3
Palestra 2: “Controle de ataques de hackers” Parte 1 / Parte 2 / Parte 3
Aula 3: “Estouros de Buffer: Explorações e Proteção” Parte 1 / Parte 2 / Parte 3
Palestra 4: “Separação de Privilégios” Parte 1 / Parte 2 / Parte 3
Palestra 5: “De onde vêm os sistemas de segurança?” Parte 1 / Parte 2
Palestra 6: “Oportunidades” Parte 1 / Parte 2 / Parte 3
Palestra 7: “Sandbox do Cliente Nativo” Parte 1 / Parte 2 / Parte 3
Aula 8: “Modelo de Segurança de Rede” Parte 1 / Parte 2 / Parte 3
Aula 9: “Segurança de aplicativos da Web” Parte 1 / Parte 2 / Parte 3
Palestra 10: “Execução Simbólica” Parte 1 / Parte 2 / Parte 3

Bom dia a todos, sou Armando Solar-Lesam e hoje darei uma palestra sobre performance simbólica. Quem dentre os presentes aqui está familiarizado com esse termo ou já ouviu falar disso antes? Eu só quero ter uma idéia do nosso público. Então, vamos começar. Larguei meu laptop várias vezes, por isso leva muito tempo para carregar.



A execução simbólica é a força de trabalho da análise moderna de programas. Esse é um dos métodos que surgiu da pesquisa e começou a ser usado em muitas aplicações. Por exemplo, hoje na Microsoft existe um sistema chamado SAGE, que funciona com muitos softwares importantes da Microsoft, variando de Power Point e terminando com o próprio Windows, para realmente encontrar problemas e vulnerabilidades de segurança.

Existem muitos projetos acadêmicos que tiveram um grande impacto no mundo real, como detectar erros importantes no software de código aberto usando execução simbólica. E a beleza da execução simbólica como técnica é que, em comparação com o teste, oferece a oportunidade de imaginar como o seu programa se comportará com um conjunto potencialmente interminável de possíveis dados de entrada. Isso nos permite investigar matrizes de dados de entrada, o que seria completamente impraticável e impraticável para investigar, digamos, por testes aleatórios, mesmo se houver um número muito grande de testadores. Por outro lado, comparado aos métodos mais tradicionais de análise estática, possui a seguinte vantagem. Ao investigar um problema, a execução simbólica pode criar entrada e rastreamento, um caminho de execução que pode ser executado em um programa real e executar este programa com base nessa entrada. E depois disso, podemos identificar o bug real e começar a corrigi-lo usando mecanismos de depuração tradicionais. E isso é especialmente valioso quando você está em um ambiente de desenvolvimento industrial em que provavelmente não tem tempo para resolver todos os pequenos problemas do seu código.

Por exemplo, você realmente deseja distinguir entre problemas reais e falsos positivos. Como isso funciona?

Para entender realmente como isso funciona, é útil começar com a execução normal. Se pensarmos na execução simbólica como uma generalização da execução tradicional e simples, faz sentido saber como ela se parece. Portanto, vou usar este programa muito simples como ilustração para muitas coisas sobre as quais falaremos hoje.



Aqui temos um trecho de um código muito simples de várias ramificações e a afirmação de que, se, sob alguma condição, o valor t <x, essa é uma afirmação falsa. Queremos descobrir se essa afirmação pode ser levantada. Isso é possível? Existe alguma entrada que fará com que esta declaração falhe?

Uma das coisas que posso fazer é verificar a execução deste programa usando valores específicos de dados de entrada como exemplo. Suponha que usemos entradas para as quais X = 4 e Y = 4. O valor de T é zero, conforme anunciado no início do programa.

Portanto, antes de chegarmos à execução normal, vamos descobrir qual é o ponto importante aqui. Precisamos ter uma ideia do estado do programa, certo? Quer estejamos executando normalmente ou simbolicamente, precisamos ter uma maneira de caracterizar o estado do programa. Nesse caso, é um programa tão simples que não usa a pilha, não usa a pilha e não há chamadas de função aqui.

Assim, o estado pode ser totalmente caracterizado por essas três variáveis, além de saber onde estou no programa. Portanto, se eu iniciar a execução de 4, 4 e 0 e chegar ao final do ramo, verificarei a expressão: 4 é maior que 4? Obviamente não.
Agora vou executar o programa em T = Y, ou seja, T não é mais 0, mas tem um valor de 4. Esse é o estado atual do meu programa e agora posso avaliar esse ramo.



É verdade que T <X? Não. Evitamos a bala, a declaração falsa não funcionou. Não houve problemas nesta execução privada.

Mas isso não nos diz nada sobre qualquer outra execução. Sabemos que com os valores X = 4 e Y = 4, o programa não falhará. Mas isso não nos diz nada sobre o que acontecerá se os valores de entrada forem 2 e 1.



Com esses valores de entrada, a execução será diferente. Desta vez, vemos que T = X e, após executar esta linha, T assumirá um valor igual a 2. Há algum problema nessa execução? Haverá um erro de afirmação com essa entrada?

Bem, vamos ver. Portanto, se T é 2 e X é 2, T não é menor que X. Parece que novamente esquivamos a bala. Certo? Portanto, aqui temos dois valores de entrada específicos nos quais o programa funciona sem erros. Mas, na verdade, ele não nos diz nada sobre outros valores de entrada.

Portanto, a ideia da execução simbólica é que queremos ir além da execução de um programa com um conjunto de dados de entrada. Queremos poder realmente falar sobre o comportamento do programa ao usar um conjunto de dados muito grande, em alguns casos, um número infinito de possíveis valores de entrada. A idéia principal disso é a seguinte.



Para um programa como esse, seu estado é determinado pelo valor dessas três variáveis ​​diferentes: X, Y e T, e sabendo onde estou no momento no programa. Mas agora, em vez dos valores específicos para X e Y, terei um valor simbólico, apenas uma variável. Uma variável que me permite nomear esse valor, que o usuário usa como entrada. Isso significa que o estado do meu programa não é mais caracterizado por corresponder nomes de variáveis ​​a valores específicos. Agora, este é um mapeamento de nomes de variáveis ​​para esses valores simbólicos.

O valor simbólico pode ser considerado como uma fórmula. Nesse caso, a fórmula para X é igual a X e a fórmula para Y é simplesmente Y, e para T é realmente igual a 0. Sabemos que, para cada valor de entrada, não importa o que você faça. O valor de T após a primeira instrução será 0.

É aí que fica interessante agora. Chegamos a esse ramo, que diz que se X for maior que Y, iremos em uma direção. Se X for menor ou igual a Y, iremos na outra direção.

Sabemos alguma coisa sobre X e Y? O que sabemos sobre eles? Pelo menos sabemos o tipo deles, sabemos que eles variam de min int a max int, mas é tudo o que sabemos sobre eles. Acontece que as informações que sabemos sobre eles não são suficientes para dizer em que direção esse ramo pode seguir. Ela pode ir em qualquer direção
Há muitas coisas que podemos fazer, mas o que podemos fazer no momento? Tente adivinhar.



Público: podemos acompanhar a execução do programa nos dois ramos.

Professor: sim, podemos acompanhar o progresso nos dois ramos. Jogue uma moeda e, dependendo de como ela cai, escolha uma ou outra ramificação.

Então, se queremos seguir os dois ramos, devemos primeiro seguir um e depois o outro, certo? Suponha que comecemos com este ramo - T = X. Sabemos que, se chegarmos a esse lugar, T terá o mesmo significado que X. Não sabemos qual é esse valor, mas temos um nome para ele - esse é o script X.



Se tomarmos o ramo oposto, o que acontecerá? O valor de T será igual a outra coisa, certo? Neste ramo, o valor de T será o valor simbólico de Y.



Então, o que esse valor T significa quando chegamos a esse ponto do programa? Talvez seja X, talvez seja Y. Não sabemos exatamente qual é esse valor, mas por que não damos um nome a ele? Chame de t ₀ . E o que sabemos sobre t ₀ ? Em que casos t ₀ será igual a X?

Essencialmente, sabemos que se X é maior que Y, então a variável é igual a X, e se X é menor que ou igual a Y, então a variável é igual a Y. Portanto, temos um valor que definimos, vamos chamá-lo de t ₀ , e ele possui esses propriedades lógicas.



Portanto, neste ponto do programa, temos um nome para o valor de T, este é t ₀ . O que fizemos aqui? Pegamos os dois ramos da instrução if e calculamos o valor simbólico, vendo sob quais condições um ramo do programa seria executado e sob o qual o outro.
Agora chega ao ponto de perguntarmos se T pode ser menor que X. Agora, o valor de T é t ₀ , e queremos saber se é possível que t ₀ seja menor que X? Lembre-se do primeiro ramo que examinamos - fizemos uma pergunta sobre X e Y e não sabíamos nada sobre eles, exceto que eram do tipo int.

Mas, com t ₀ , sabemos muito sobre isso. Sabemos que, em alguns casos, será igual a X e, em alguns casos, será igual a Y. Portanto, agora ele nos fornece um conjunto de equações que podemos resolver. Então, podemos dizer se é possível que t _{0 seja} menor que X, sabendo que t ₀ satisfaz todas essas condições? Assim, podemos expressar isso como uma restrição, mostrando se é possível que t ₀ seja menor que X. E se X é maior que Y, então t ₀ é igual a X e se X é menor ou igual a Y, isso significa que t ₀ = Y.



Então, temos uma equação. Se houver uma solução, se for possível encontrar o valor de t ₀ , o valor de X e o valor de Y que satisfazem essa equação, então reconhecemos esses valores e, quando os inserimos no programa, quando executado, ele percorre esse ramo se t <x e " irá explodir ”quando cair em afirmar falso.

Então, o que fizemos aqui? Executamos o programa, mas, em vez de mapear nomes de variáveis ​​para valores específicos, atribuímos valores simbólicos a esses nomes de variáveis. De fato, eles deram outros nomes de variáveis. E, nesse caso, nossos outros nomes de variáveis ​​são o script X, o script Y, t ₀ e, além disso, temos um conjunto de equações que mostram como esses valores estão relacionados. Temos uma equação que nos diz como t ₀ está relacionado a X e Y neste caso.

A solução desta equação nos permite responder à pergunta se esse ramo pode ser executado ou não. Dê uma olhada na equação - é possível pegar esse ramo ou não? Parece que não, porque estamos procurando casos em que t _{0 é} menor que X, mas se na primeira condição t ₀ = X, a expressão t ₀ <X não será verdadeira.

Portanto, isso significa que, quando X> Y, isso não pode acontecer, porque t ₀ = X e não pode ser igual ou menor que X ao mesmo tempo.

Mas o que acontece se t ₀ = Y? T ₀ pode ser menor que X neste caso?

Não, definitivamente não pode, porque sabemos que X <Y. Portanto, se t ₀ é menor que X, também será menor que Y. Mas sabemos que, neste caso, t ₀ = Y. E, portanto, novamente , essa condição não pode ser satisfeita. Portanto, aqui temos uma equação que não tem solução, e não importa quais valores você inclua nessa equação.

Você não pode resolvê-lo, e isso nos diz que, independentemente das entradas X e Y que passamos para o programa, ele não será desativado se t <x.

Agora observe que, ao criar esse argumento aqui, eu basicamente sugeri sua intuição sobre números inteiros, sobre números matemáticos. Na prática, sabemos que as entradas da máquina não se comportam exatamente como as entradas matemáticas. Há casos em que as leis aplicadas aos tipos de dados inteiros matemáticos não são aplicáveis ​​às entradas programáticas.

Portanto, devemos ter muito cuidado ao resolver essas equações, porque devemos lembrar que esses não são os números inteiros sobre os quais fomos informados no ensino fundamental. Esses são os números inteiros de 32 bits usados ​​pela máquina. E há muitos casos de erros que ocorreram porque os programadores pensaram em seu código em termos de números matemáticos, sem perceber que existem coisas como estouros que podem causar comportamento diferente do programa para entrada matemática.

Outra coisa que descrevi aqui é um argumento puramente intuitivo. Vou guiá-lo pelo processo, mostrando como fazê-lo manualmente, mas isso não é de forma alguma um algoritmo. A beleza dessa idéia de execução simbólica, no entanto, é que ela pode ser codificada em um algoritmo. E você pode resolvê-lo mecanicamente, o que permite fazer isso não apenas para um programa de 10 linhas, mas para milhões de programas. Isso nos permite usar o mesmo raciocínio intuitivo que usamos neste caso e falar sobre o que acontece quando executamos este programa com diferentes valores de entrada. E essas considerações podem ser dimensionadas e estendidas para programas muito grandes.



Público: e se o programa não suportar a entrada de um determinado tipo de variável?

Professor: esta é uma pergunta muito boa! Suponha que tenhamos o mesmo programa, mas, em vez de t = x, teremos t = (x-1). Então, intuitivamente, podemos imaginar que agora esse programa pode "explodir", certo?



Porque quando o programa segue esse caminho, t realmente será menor que x. O que acontecerá com esse programa? Como será nosso estado simbólico? Qual será t ₀ quando x for maior que y? Corrigimos as linhas em nossas equações de acordo com outro valor quando t = (x-1). Agora o programa pode falhar, e você vai ao desenvolvedor e diz a ele: “ei, essa função pode explodir quando x for maior que y”!

O desenvolvedor analisa isso e diz: “Ah, esqueci de lhe dizer - na verdade, essa função nunca será chamada com parâmetros, onde x é maior que y. "Acabei de escrever por alguns motivos históricos, então não se preocupe, eu não me lembraria se você não tivesse me contado."

Suponha que tenhamos uma suposição de que x será menor ou igual a y.



Esta é uma pré-condição ou acordo para nossa função. A função promete fazer algo, mas apenas se o valor satisfizer essa suposição. Mas se não for satisfeita, a função diz: "Eu não ligo para o que acontece. Eu prometo que não haverá erro apenas se essa suposição for cumprida. "

Então, como codificamos essa restrição quando resolvemos as equações? Essencialmente, temos um conjunto de restrições que nos dizem se esse ramo é viável. Além das limitações, devemos também garantir que a pré-condição ou suposição seja atendida.

A questão é: posso encontrar xey que atendam a todas essas restrições e, ao mesmo tempo, possuam as propriedades necessárias? Você pode ver que essa restrição X ≤ Y representa a diferença entre o caso em que essa restrição é atendida e o caso em que não é atendida.

Essa é uma questão muito importante ao trabalhar com análise, especialmente quando você deseja fazer isso simultaneamente no nível das funções individuais. É aconselhável saber o que o programador tinha em mente ao escrever esta função. Como se você não tem idéia sobre essas suposições, pode pensar que há alguma entrada de que o programa falhará.

Como fazer isso de maneira mecânica? Existem dois aspectos para esse problema. Aspecto número um - como você realmente criou essas fórmulas?

Nesse caso, é intuitivamente claro como chegamos a essas fórmulas, simplesmente as compusemos manualmente. Mas como criar essas fórmulas mecanicamente?

E o segundo aspecto - como você resolve essas fórmulas depois de tê-las? É possível realmente resolver essas fórmulas que descrevem se o seu programa falha ou não?
Vamos começar com a segunda pergunta. Podemos reduzir nosso problema com essas fórmulas, que incluem raciocínio inteiro e vetores de bits. Ao criar programas, você cuida de matrizes, funções e, como resultado, obtém fórmulas gigantes. É possível resolvê-los mecanicamente?



As muitas tecnologias sobre as quais estamos falando hoje são ferramentas práticas relacionadas aos tremendos avanços no desenvolvimento de solucionadores de questões lógicas. Em particular, existe uma classe muito importante de solucionadores, chamada SMT, ou o "solucionador de solvabilidade de teorias modulares". O solucionador SMT é a solvabilidade das fórmulas lógicas, levando em consideração as teorias subjacentes a elas.

Muitas pessoas afirmam que esse nome não é particularmente bom, mas foi corrigido como o mais usado.

O SMT-solver é um algoritmo devido ao qual essa fórmula lógica na saída fornecerá uma das duas opções: ela satisfaz sua finalidade ou não.O segundo caso significa que nesta fórmula é impossível usar os valores das variáveis ​​que atendem aos requisitos das restrições definidas.

Na prática, isso parece um pouco assustador e um pouco mágico. A maioria dos problemas que o SMT deve resolver são problemas completos de NP, ou seja, tarefas com a resposta "sim" ou "não".
Podemos ter um sistema que se baseie na solução de problemas completos de NP como seu principal componente? Ou precisamos de outra coisa que funcione na prática? O fato é que muitos solucionadores de SMT também têm uma terceira resposta possível: "Eu não sei".



, , , , : « ». , , .

27:30

MIT « ». 10: « », 2


A versão completa do curso está disponível aqui .

, . ? ? , 30% entry-level , : VPS (KVM) E5-2650 v4 (6 Cores) 10GB DDR4 240GB SSD 1Gbps $20 ? ( RAID1 RAID10, 24 40GB DDR4).

VPS (KVM) E5-2650 v4 (6 núcleos) 10GB DDR4 240GB SSD de 1Gbps até dezembro de graça quando pagar por um período de seis meses, você pode fazer o pedido aqui .

Dell R730xd 2 ? 2 Intel Dodeca-Core Xeon E5-2650v4 128GB DDR4 6x480GB SSD 1Gbps 100 $249 ! . c Dell R730xd 5-2650 v4 9000 ?