Engenheiros da SEAS trabalham em prol de uma computação à prova de hackers

A cada poucos dias, as notícias nos trazem histórias de violações massivas de dados, resultando no roubo de grandes quantidades de dinheiro ou na divulgação de informações confidenciais. Quer você esteja fazendo uma transação on-line de rotina ou votando em uma eleição nacional, a questão da segurança cibernética mantém todos sob vigilância.

À medida que a tecnologia avança, os hackers encontram novos meios de explorá-la. É um problema que requer estratégias em diversas frentes e repensar abordagens de software, hardware e legislação. Na SEAS, vários membros do corpo docente estão explorando a questão de como tornar a computação mais segura e confiável.

Um sistema operacional à prova de hackers

Idealmente, o sistema operacional de um computador teria em seu núcleo um kernel pequeno e confiável que pudesse gerenciar todos os recursos de hardware e também fornecer isolamento e proteção para diferentes componentes de software. Mas os sistemas operacionais são complicados e apenas uma falha no código pode escapar à detecção por seus criadores e deixar o sistema vulnerável a hackers. Eliminar completamente essas falhas, entretanto, é extremamente desafiador.

“A evolução dos sistemas informáticos tem sido fortemente influenciada por considerações empresariais – as pessoas querem ser as primeiras no mercado”, disse Zhong Shao, professor e chefe do departamento de ciência da computação. Para economizar tempo, os desenvolvedores muitas vezes contam com código legado, uma prática que parecia boa quando ninguém imaginava que os computadores desempenhariam um papel tão importante em nossas vidas. Agora, com tantas plataformas diferentes em utilização, a Internet das Coisas a decolar e os carros autónomos ao virar da esquina, precisamos de maior garantia de que os nossos sistemas operativos são seguros e fiáveis.

Para isso, Shao está liderando uma equipe na construção do CertiKOS (Certified Kit Operating System). É um sistema operacional baseado em verificação formal, no qual os componentes interdependentes do kernel são cuidadosamente desembaraçados e especificações matemáticas são escritas para o comportamento pretendido de cada módulo do kernel. Para fazer isso, eles estruturam o kernel usando camadas de abstração certificadas e projetam cada componente para que possa ser formalmente verificado separadamente e vinculado pela estrutura da camada.

Isso difere da forma convencional de verificar a confiabilidade de um programa, na qual o desenvolvedor do software testa o programa em vários cenários. Uma das coisas que diferencia o CertiKOS de outros sistemas verificados anteriormente é que ele é um sistema operacional simultâneo, que permite rodar em computadores com múltiplos processadores. Para software complexo com simultaneidade, o teste não pode mais cobrir o espaço de estado do programa, portanto não pode eliminar todos os bugs do sistema.

A computação atingiu um ponto em que permitir a possibilidade de erros não é mais aceitável. Shao compara um sistema operacional a um governo, que também possui várias camadas e gerencia e facilita processos. A sua estrutura também significa que a corrupção em apenas uma camada pode prejudicar outras também.

“A abordagem CertiKOS consiste em aplicar técnicas formais de princípios para decompor esses sistemas muito complexos em muitas camadas de abstração cuidadosamente projetadas”, disse Shao. “Para cada componente complexo, você tenta descobrir sua estrutura semântica. Construímos o sistema operacional de forma limpa, camada por camada.”

Se as camadas não estiverem organizadas de maneira consistente, disse Shao, você provavelmente criará uma base ruim para quaisquer novos recursos. Porém, se você realmente entender os fundamentos semânticos desses diferentes recursos, eles poderão servir como base para um sistema que seja mais extensível — isto é, capaz de assumir novos recursos e ser adaptado para diferentes domínios de aplicação.

Um grande desafio do projeto é garantir que não seja visto como um exercício acadêmico, disse Shao. Isso significa expandir o ecossistema CertiKOS a ponto de poder ser implantado em muitos domínios de aplicação realistas. “Ainda precisamos de engenheiros para tornar o produto mais abrangente e aplicá-lo a mais plataformas”, disse ele. “Caso contrário, as pessoas não levarão isso a sério.”

Shao reconhece que o projeto é bastante ambicioso e que o novo ecossistema CertiKOS pode perturbar e transformar a forma como a indústria da informática funciona há décadas. Mas ele também sabe que a forma atual de fazer as coisas é insustentável.

“Para o futuro, precisamos construir um novo ecossistema de sistema operacional que seja super limpo e forneça uma garantia livre de bugs e à prova de hackers”, disse ele. “Caso contrário, o mundo cibernético, os carros autônomos, as IoTs, as blockchains e o futuro da inteligência artificial poderão enfrentar sérios problemas.”

Protegendo seu voto

Acompanhar o campo em constante transformação do conflito cibernético tem se mostrado complicado em muitas áreas, incluindo a jurídica. Para esse fim, Joan Feigenbaum, Professora Grace Murray Hopper de Ciência da Computação e Economia, uniu-se aos professores Oona Hathaway e Scott Shapiro da Escola de Direito de Yale para trabalhar em novas formas de pensar sobre segurança cibernética.

A colaboração, financiada com uma doação de dois anos de US$ 406.000 da Fundação William e Flora Hewlett, inclui o curso “A Lei e a Tecnologia do Conflito Cibernético”. No primeiro semestre, os alunos (10 de direito e 11 de informática) se reuniram para seminários semanais. No segundo semestre, os alunos trabalharam individualmente e em equipes em projetos que abordam questões urgentes de conflitos cibernéticos. Uma equipe de estudantes, Sahil Gupta, Patrick Lauppe e Shreyas Ravishankar, desenvolveu uma criptomoeda que eles chamam de “FedCoin”. É semelhante ao BitCoin, mas seria sancionado pelo Federal Reserve ou pelo banco central de qualquer país. Possuiria as propriedades de segurança da criptografia moderna com as propriedades legais e sociais das moedas convencionais.

Outra equipe, composta pelos estudantes de ciência da computação Soham Sankaran, Sachith Gullapalli e Lincoln Swaine-Moore, assumiu um projeto particularmente oportuno. Concentraram-se no desenvolvimento de um sistema que permita aos eleitores verificar se os seus votos foram registados e contados correctamente, sem permitir o acesso a informações sobre os boletins de voto de outros eleitores. Anteriormente, os investigadores Tal Moran e Mori Naor tinham demonstrado que este sistema poderia funcionar em teoria, mas não tinham construído um sistema baseado nas suas ideias. Para ver como isso se sairia na vida real — idealmente, à escala de uma eleição nacional — os três estudantes desenvolveram o seu próprio sistema para demonstrar que poderia funcionar na prática.

Tomando os artigos publicados por Moran e Naor, os alunos implementaram a criptografia e a interface que compunham o sistema teórico de emissão, contagem e verificação de votos. Eles também adicionaram alguns novos recursos, incluindo um sistema para verificar recibos e assinaturas de recibos. É um acréscimo crucial, uma vez que Moran e Naor reconheceram que o seu sistema teórico era vulnerável a eleitores corruptos que poderiam concebivelmente falsificar recibos eleitorais ou diminuir a legitimidade de uma eleição “gritando o lobo” sobre recibos falsos. Seu sistema incorpora recibos que contêm “compromissos” de voto – ou seja, pequenas informações determinadas pelo voto. Estes compromissos poderiam ser usados ​​pelo eleitor (que já sabe como votou) para fins de verificação, mas provavelmente não teriam utilidade para alguém que não conhecesse o voto emitido pelo eleitor real.

O próximo passo do projeto é testar o sistema em uma eleição com eleitores reais e ver o quão intuitiva é a interface para quem não conhece o sistema. Eles também gostariam de tornar o sistema de código aberto para obter feedback da comunidade e permitir que outros personalizem o sistema de acordo com suas necessidades específicas.

A “impressão digital” exclusiva de um dispositivo eletrônico poderia ser usada para torná-lo mais seguro?

Melhor segurança a partir da ‘impressão digital’ de um dispositivo

Todos os dispositivos eletrônicos — mesmo os mesmos produtos dos mesmos fabricantes — possuem variações únicas em seu hardware. Jakub Szefer, professor assistente de engenharia elétrica, acredita que pode usar essas variações para criar segurança adicional para os usuários desses dispositivos.

O projeto de Szefer, pelo qual ele ganhou o prêmio de Desenvolvimento de Carreira em Início de Carreira (CAREER) da National Science Foundation este ano, concentra-se no uso da “impressão digital” de hardware de um dispositivo para aumentar a segurança dos dispositivos de computação do dia a dia. Quase todos os dispositivos de computação, smartphones ou dispositivos da Internet das Coisas dependem de um sistema de armazenamento de dados conhecido como memória dinâmica de acesso aleatório (DRAM). A carga nos capacitores de armazenamento da célula DRAM se dissipa com o tempo, portanto, é necessário um mecanismo de atualização para recarregar os capacitores e manter os dados armazenados.

Quando um fabricante fabrica o chip DRAM, o processo de fabricação pode resultar em diferentes comprimentos de fio, alterações na espessura dos capacitores e outras variações microscópicas. Essas diferenças são muito pequenas, mas suficientes para fazer com que cada DRAM tenha seu próprio comportamento de decaimento.

“Quando você desliga o mecanismo de atualização, os dados decaem, mas diferentes células DRAM decaem em taxas diferentes – é aí que entra a impressão digital”, disse Szefer. “A taxa de decaimento da coleção de células DRAM é única para cada modelo, como resultado das variações de fabricação.”

A singularidade de cada dispositivo pode ser usada para torná-lo mais seguro. Por exemplo, um usuário de iPhone agora pode fazer login em um site bancário usando uma senha – que pode ser roubada. Mas se o sistema de segurança também incluir a impressão digital do hardware do dispositivo, alguém precisaria da senha e do próprio iPhone do usuário para entrar no site do banco.

As ideias que surgem da pesquisa podem ser prontamente implementadas, uma vez que o projeto centra-se em hardware já presente nos dispositivos. Colocar a impressão digital em uso prático, entretanto, faz parte do desafio do projeto. Para evitar desabilitar completamente o mecanismo de atualização, o que tornaria o dispositivo inútil, Szefer precisa desabilitar seletivamente algumas regiões da DRAM, evitando que os dados em outras regiões se deteriorem. Dessa forma, eles poderão ler a impressão digital, mas o restante da DRAM será atualizado e o dispositivo poderá continuar funcionando.

O projeto também poderia aproveitar as propriedades físicas do hardware do computador para desenvolver novas versões de protocolos criptográficos baseadas em hardware. Por exemplo, poderia incorporar o que é conhecido como Transferência Esquecida, na qual duas partes podem trocar certas informações, mas manter outras em segredo. Esses protocolos foram incorporados a programas de software, mas são baseados puramente em diferentes modelos matemáticos decadentes que poderiam, teoricamente, ser quebrados por um hacker inteligente. Szefer disse que entrelaçar os protocolos criptográficos com o hardware de um dispositivo poderia criar mais uma camada de segurança.

Outra possibilidade que Szefer está explorando é usar essa tecnologia para criar um sistema para verificar se um dispositivo é falsificado ou não – um problema que afeta principalmente os eletrônicos menores. Por exemplo, o fabricante poderia obter a impressão digital de cada dispositivo produzido. Poderia então ser criado um sistema que permitisse aos consumidores verificar a autenticidade dos seus dispositivos.

Manutenção da privacidade e chips autocorretivos

Quando duas partes compartilham dados em grande escala, nem sempre é fácil controlar quais informações são divulgadas e quais são mantidas em sigilo. Com o objetivo de mudar isso, a professora assistente de ciência da computação Mariana Raykova está trabalhando em um programa que permite que vários usuários compartilhem dados sem entrar em conflito com questões de privacidade e restrições legais.

Raykova, que recebeu este ano o Google Faculty Research Award pelo projeto, observou que muitas vezes existem acordos legais entre as partes que estipulam que apenas um subconjunto de dados que faz parte de um conjunto maior de dados pode ser usado. Mas saber com certeza que estes acordos serão honrados é uma questão complicada. Num cenário, dois ou três hospitais podem precisar de partilhar informações sobre um procedimento médico específico de um paciente. Devido à HIPAA e outras questões de privacidade, entretanto, os outros dados médicos do paciente não devem ser abertos às três partes. O grupo de Raykova está desenvolvendo técnicas criptográficas que permitem às diversas partes projetar um modelo que atenda às suas necessidades específicas.

Exatamente como o Google faz uso de seus dados é proprietário, mas Raykova disse que há várias maneiras pelas quais o projeto de sua equipe poderia beneficiar o gigante dos mecanismos de busca. O Google coleta uma enorme quantidade de dados relacionados ao usuário e depois aplica aprendizado de máquina técnicas para construir modelos que expliquem claramente o comportamento desses usuários. Freqüentemente, os dados vêm de múltiplas fontes. Alguns anunciantes do Google, por exemplo, querem ter uma ideia melhor da eficácia de seus anúncios: os usuários acessam o site da empresa, por exemplo, ou compram seus produtos? Por outro lado, essas empresas podem ter dados úteis para o Google sobre as pessoas que usam o mecanismo de busca.

Raykova disse que a mesma tecnologia poderia ser aplicada a vários outros usos, como bancos de dados fiscais e judiciais. Um dos principais desafios no desenvolvimento destas técnicas é torná-las eficientes, disse ela, uma vez que traduzir uma computação regular numa computação segura pode consumir muito tempo de computação e outros recursos.

Ela também está trabalhando em outra preocupação urgente de segurança: chips com circuitos integrados (IC) defeituosos ou maliciosos. É um problema que acontece quando os projetistas de semicondutores terceirizam circuitos para fabricantes possivelmente não confiáveis. Devido à complexidade de certos chips, falhas nesses circuitos terceirizados podem passar despercebidas pelos desenvolvedores, mas podem acabar prejudicando o produto. As soluções atuais estão limitadas a obrigações legais e contratuais ou a testes de IC pós-fabricação – nenhuma delas é considerada adequada.

O projeto, intitulado “Hardware verificável: chips que provam sua própria correção”, ganhou uma doação de US$ 3 milhões da National Science Foundation. Além de Raykova, o projeto inclui pesquisadores da Universidade da Virgínia; Universidade de Nova York; Universidade da Califórnia, San Diego; e CUNY City College.

Os pesquisadores estão analisando os benefícios mais amplos de seu projeto, desenvolvendo novas abordagens práticas para o problema da computação geral verificável. Hardware verificável, dizem eles, é fundamental para a construção de futuros sistemas de computação que sejam confiáveis ​​e livres de grandes falhas de segurança. Em última análise, o objetivo deles é usar ferramentas de código aberto para tornar o hardware verificável acessível para uso em aplicações de hardware criptográfico.