Avançando a Segurança em Computação Multi-Partidária

A Computação Segura de Múltiplas Partes (MPC) é uma ferramenta chave pra manter os dados privados no nosso mundo interconectado. Ela permite que diferentes partes trabalhem juntas sem revelar seus dados particulares umas às outras. Mas, provar que esses protocolos de MPC de baixo nível são seguros geralmente depende de métodos manuais que podem ser complexos e cheios de erros. Isso é um problema porque os métodos pra verificar esses protocolos não são padronizados, dificultando a vida de muitos especialistas em linguagens de programação.

Pra facilitar esse processo, criamos uma nova linguagem de programação que ajuda a definir vários protocolos de MPC de baixo nível. Essa nova linguagem também inclui maneiras de checar Confidencialidade e Integridade - duas características de segurança importantes. As checagens que a gente propõe são parecidas com as encontradas em modelos tradicionais de fluxo de informação, que ajudam a garantir que informações sensíveis não vazem. Mostramos como nossa nova linguagem se conecta com modelos de segurança de MPC padrão e como elas podem ser usadas juntas pra verificar a segurança desses protocolos de forma mais eficiente.

#Importância da Programação de MPC de Baixo Nível

Linguagens de programação de alto nível são feitas pra ajudar a criar aplicações completas. Elas focam em tornar a programação mais fácil e eficaz. Mas, quando o assunto é MPC, muitas linguagens de alto nível usam protocolos de baixo nível pra gerenciar o compartilhamento e processamento de dados. Esses protocolos de baixo nível, que incluem compartilhamento secreto e outros métodos, precisam de uma verificação manual cuidadosa. O desafio é que tanto designs de linguagens de alto nível quanto de baixo nível são necessários pra garantir que os protocolos de MPC sejam seguros.

A interação entre como a informação flui e quão seguros os protocolos de MPC são fica complicada, especialmente no nível baixo. No MPC, vários clientes se comunicam pra calcular e compartilhar resultados sem precisar de um terceiro confiável. Esse processo de compartilhamento pode acidentalmente revelar algumas informações sobre os inputs privados, mesmo quando os resultados gerais permanecem seguros. A funcionalidade ideal no MPC deve traçar uma política pra lidar com essa informação corretamente, e fazer isso pode ser complicado.

#Visão Geral das Nossas Contribuições

Este trabalho apresenta um sistema em três partes pra verificar protocolos de MPC:

1. Uma nova linguagem de programação de baixo nível feita pra definir operações básicas de MPC.
2. Uma maneira automatizada de verificar operações de MPC de baixo nível nessa nova linguagem.
3. Um método semi-automatizado pra checar a segurança de protocolos de MPC maiores que se baseiam nessas operações de baixo nível.

Além disso, definimos um conjunto de propriedades de segurança que podem interessar especialistas na área.

#Design da Linguagem pra MPC

Desenvolvemos uma nova linguagem de programação pra ajudar a definir protocolos distribuídos. Essa linguagem permite mensagens síncronas entre clientes que fazem parte do protocolo. Também criamos uma metalinguagem que gera protocolos dinamicamente. Isso dá aos programadores a habilidade de expressar conceitos de baixo nível facilmente.

A sintaxe da nossa linguagem de programação é simples. Ela suporta operações padrão como adição, subtração e multiplicação dentro de um campo finito. Os clientes enviam mensagens e revelam informações de um jeito que se encaixa na estrutura dessa linguagem. Isso facilita a escrita, compreensão e verificação de protocolos de MPC.

#Modelo de Segurança pra MPC

Os protocolos de MPC têm como objetivo fornecer resultados sem vazar mais informações do que o necessário. Com nosso novo modelo de segurança, conseguimos classificar as saídas desses protocolos em dois tipos: real e ideal. O conceito chave é que o protocolo real não deve revelar mais informações do que o modelo ideal revelaria na mesma situação.

Em um modelo de segurança básico, supõe-se que todos os clientes sigam as regras dos protocolos. Podemos dizer que um protocolo é "correto" se, pra qualquer entrada dada, ele produz a saída esperada sem revelar informações extras. Esse nível de segurança passiva pode ser definido probabilisticamente, usando funções matemáticas que expressam como as variáveis de entrada e saída se relacionam.

Quando pensamos em clientes maliciosos - que escolhem quebrar as regras - introduzimos uma maneira de detectar qualquer trapaça que possa ocorrer. Isso adiciona mais uma camada de segurança ao nosso modelo. Participantes honestos devem conseguir identificar esse comportamento inadequado e abortar a operação se necessário.

#Propriedades de Segurança pra MPC

Criamos várias propriedades de segurança pra avaliar a segurança dos protocolos de MPC. Uma propriedade chave é conhecida como não-interferência condicional, que mantém que observar os resultados do protocolo não deve dar ao observador nenhum insight extra sobre os inputs privados compartilhados.

Outra propriedade é liberação gradual. Isso significa que o protocolo deve liberar apenas uma pequena quantidade de informações de cada vez, mantendo outros detalhes sensíveis escondidos. Também discutimos a desclassificação robusta, que garante que mesmo que algumas informações sejam reveladas, elas permaneçam dentro dos limites acordados previamente pelo protocolo.

#Técnicas de Verificação pra MPC

Pra verificar a segurança dos protocolos de MPC, desenvolvemos métodos que nos permitem determinar se certas propriedades são verdadeiras. Esse processo de verificação pode ser totalmente automatizado para protocolos simples, enquanto pra protocolos mais complexos, um método semi-automatizado pode ajudar na verificação.

Nossos métodos podem determinar a distribuição de probabilidade dos resultados de diferentes execuções de protocolo, permitindo checagens de segurança que são orientadas por dados. Usando essas abordagens, conseguimos verificar protocolos do mundo real, como aqueles usados em aplicações focadas em privacidade, como votação segura ou compartilhamento confidencial de dados.

#Implicações Práticas e Trabalho Futuro

A nova linguagem de programação que desenhamos, junto com nossa exploração das propriedades de segurança, estabelece as bases pra definir melhor os protocolos de MPC de baixo nível. Também abre portas pra melhorar a verificação de segurança. Existem muitas áreas que podemos explorar mais, que podem levar a melhores ferramentas e métodos pra garantir que esses protocolos sejam seguros e confiáveis.

Uma área promissora pra pesquisas futuras é integrar nossas técnicas de verificação com assistentes de prova existentes. Isso permitiria que programadores escrevessem protocolos mais seguros com menos esforço. Além disso, expandir nossa linguagem pra lidar com concorrência de forma eficaz nos permitiria capturar práticas comuns de MPC, como compartilhamento de compromissos e otimização de circuitos, de maneira mais completa.

#Conclusão

Nosso trabalho contribui pra tornar a computação segura de múltiplas partes mais acessível através do desenvolvimento de uma linguagem de programação especializada e um processo de verificação sistemático. Focando em protocolos de baixo nível e integrando melhorias na forma como gerenciamos a segurança, pretendemos aprimorar a maneira como dados sensíveis podem ser tratados e protegidos em ambientes colaborativos. As percepções obtidas a partir deste trabalho podem ajudar a pavimentar o caminho pra métodos mais seguros e eficientes no campo crescente da privacidade de dados.