Avanzando la seguridad en la computación multiparte

La Computación Segura Multi-Partes (MPC) es una herramienta clave para mantener la privacidad de los datos en nuestro mundo interconectado. Permite que diferentes partes trabajen juntas sin revelar su información privada entre sí. Sin embargo, demostrar que estos protocolos MPC de bajo nivel son seguros a menudo depende de métodos manuales que pueden ser complejos y propensos a errores. Este es un problema porque los métodos para verificar estos protocolos no están estandarizados, lo que dificulta que muchos expertos en lenguajes de programación puedan trabajar con ellos.

Para facilitar este proceso, hemos creado un nuevo lenguaje de programación que ayuda a definir varios protocolos MPC de bajo nivel. Este nuevo lenguaje también incluye formas de comprobar la Confidencialidad y la Integridad, que son dos características importantes de seguridad. Las verificaciones que proponemos son similares a las que se encuentran en los modelos tradicionales de flujo de información, que ayudan a garantizar que la información sensible no se filtre. Mostramos cómo nuestro nuevo lenguaje se conecta con los modelos de seguridad MPC estándar y cómo se pueden usar juntos para verificar la seguridad de estos protocolos de manera más efectiva.

#Importancia de la Programación de Bajo Nivel en MPC

Los lenguajes de programación de alto nivel están diseñados para ayudar a crear aplicaciones completas. Se enfocan en hacer la programación más fácil y efectiva. Sin embargo, cuando se trata de MPC, muchos lenguajes de alto nivel utilizan protocolos de bajo nivel para gestionar el intercambio y procesamiento de datos. Estos protocolos de bajo nivel, que incluyen el intercambio de secretos y otros métodos, requieren una verificación manual cuidadosa. El desafío es que se necesitan diseños de lenguajes de alto y bajo nivel para asegurar que los protocolos MPC sean seguros.

La interacción entre cómo fluye la información y cuán seguros son los protocolos MPC se complica, especialmente a bajo nivel. En MPC, varios clientes se comunican entre sí para calcular y compartir resultados sin necesidad de un tercero de confianza. Este proceso de compartición puede revelar accidentalmente algo de información sobre las entradas privadas, incluso cuando los resultados generales siguen siendo seguros. La funcionalidad ideal en MPC debe delinear una política para manejar esta información correctamente, y hacerlo puede ser complicado.

#Resumen de Nuestras Contribuciones

Este trabajo introduce un sistema de tres partes para verificar protocolos MPC:

1. Un nuevo lenguaje de programación de bajo nivel diseñado para definir operaciones básicas de MPC.
2. Una forma automatizada de verificar operaciones MPC de bajo nivel en este nuevo lenguaje.
3. Un método semi-automatizado para comprobar la seguridad de protocolos MPC más grandes que se basan en estas operaciones de bajo nivel.

Además, definimos un conjunto de propiedades de seguridad que pueden interesar a los expertos en el campo.

#Diseño del Lenguaje para MPC

Desarrollamos un nuevo lenguaje de programación para ayudar a definir protocolos distribuidos. Este lenguaje permite el envío de mensajes de manera sincrónica entre los clientes que forman parte del protocolo. También creamos un metalenguaje que genera protocolos de forma dinámica. Esto le da a los programadores la capacidad de expresar fácilmente conceptos de bajo nivel.

La sintaxis de nuestro lenguaje de programación es sencilla. Soporta operaciones estándar como suma, resta y multiplicación dentro de un campo finito. Los clientes envían mensajes y revelan información de una manera que encaja en el marco de este lenguaje. Esto facilita la escritura, comprensión y verificación de protocolos MPC.

#Modelo de Seguridad para MPC

Los protocolos MPC tienen como objetivo proporcionar resultados sin filtrar más información de la necesaria. Con nuestro nuevo modelo de seguridad, podemos clasificar las salidas de estos protocolos en dos tipos: real e ideal. El concepto clave es que el protocolo real no debe revelar más información que la que el modelo ideal revelaría en la misma situación.

En un modelo de seguridad básico, se asume que todos los clientes siguen las reglas de los protocolos. Podemos decir que un protocolo es "correcto" si, para cualquier entrada dada, produce la salida esperada sin revelar información extra. Este nivel de seguridad pasiva puede definirse probabilísticamente, usando funciones matemáticas que expresan cómo se relacionan las variables de entrada y salida entre sí.

Al considerar clientes malintencionados-que eligen romper las reglas-introducimos una forma de detectar cualquier trampa que pueda ocurrir. Esto añade otra capa de seguridad a nuestro modelo. Los participantes honestos deberían poder detectar este comportamiento deshonesto y abortar la operación si es necesario.

#Propiedades de Seguridad para MPC

Hemos creado diversas propiedades de seguridad para evaluar la seguridad de los protocolos MPC. Una propiedad clave se conoce como no interferencia condicional, que sostiene que observar los resultados del protocolo no debería dar al observador ninguna información extra sobre las entradas privadas que se están compartiendo.

Otra propiedad es la liberación gradual. Esto significa que el protocolo solo debería liberar una pequeña cantidad de información a la vez, manteniendo otros detalles sensibles ocultos. También discutimos la desclasificación robusta, que asegura que incluso si se revela algo de información, se mantenga dentro de los límites acordados previamente por el protocolo.

#Técnicas de Verificación para MPC

Para verificar la seguridad de los protocolos MPC, desarrollamos métodos que nos permiten determinar si ciertas propiedades son verdaderas. Este proceso de verificación puede ser totalmente automatizado para protocolos simples, mientras que para los más complejos, un método semi-automatizado puede asistir en la verificación.

Nuestros métodos pueden determinar la distribución de probabilidad de los resultados provenientes de diferentes ejecuciones del protocolo, permitiendo verificaciones de seguridad que están basadas en datos. Al usar estos enfoques, podemos verificar protocolos del mundo real como los que se utilizan en aplicaciones enfocadas en la privacidad, como la votación segura o el intercambio confidencial de datos.

#Implicaciones Prácticas y Trabajo Futuro

El nuevo lenguaje de programación que diseñamos, junto con nuestra exploración de propiedades de seguridad, sienta las bases para definir mejor los protocolos MPC de bajo nivel. También abre la puerta a mejorar la verificación de seguridad. Hay muchas áreas que podemos explorar más a fondo, lo que puede llevar a mejores herramientas y métodos para garantizar que estos protocolos sean seguros y confiables.

Una área prometedora para la investigación futura es integrar nuestras técnicas de verificación con asistentes de prueba existentes. Esto permitiría a los programadores escribir protocolos más seguros con menos esfuerzo. Además, expandir nuestro lenguaje para manejar la concurrencia de manera efectiva nos permitiría capturar prácticas comunes de MPC, como el intercambio de compromisos y la optimización de circuitos, de manera más completa.

#Conclusión

Nuestro trabajo contribuye a hacer que la computación segura multi-partes sea más accesible a través del desarrollo de un lenguaje de programación especializado y un proceso sistemático de verificación. Al enfocarnos en protocolos de bajo nivel e integrar mejoras en la gestión de seguridad, buscamos mejorar la forma en que se puede manejar y proteger la información sensible en entornos colaborativos. Los conocimientos obtenidos a partir de este trabajo pueden ayudar a allanar el camino para métodos más seguros y eficientes en el campo en expansión de la privacidad de los datos.