Quel est le lien entre l'informatique théorique et la sécurité?

Quand je pense à un logiciel qui n'est pas sûr, je pense qu'il est "trop ​​utile" et peut être utilisé abusivement par un attaquant. Donc, dans un sens, la sécurisation des logiciels est le processus qui rend les logiciels moins utiles. En informatique théorique, vous ne travaillez pas avec le monde réel. Y a-t-il donc des problèmes de sécurité lorsque vous travaillez avec de la théorie pure? Ou de l'autre côté de la médaille, l'informatique théorique affecte-t-elle le monde réel des personnes piratées? Si oui, quels sujets de sécurité sont considérés comme théoriques?

Votre intuition que "l'insécurité" est due à un logiciel "trop ​​utile" est correcte, dans un sens. Il existe une littérature théorique importante et croissante sur la «confidentialité différentielle» qui formalise votre intuition. Voir par exemple ici: research.microsoft.com/en-us/projects/databaseprivacy/dwork.pdf

$\epsilon$$e^\epsilon$

$0$

De nombreuses façons différentes:

• Cryptographie (une généralisation extrêmement large de la sécurité des informations qui va de la confidentialité au cryptage)
• Vérification formelle du code (voir aussi le projet seL4 )
• Tolérance aux pannes et correction des erreurs
• Moyens théoriques pour empêcher les logiciels malveillants ( un autre ), y compris la signature de code
• Matériel inviolable
• Obfusation ponctuelle (approche théorique de l'obfusaction de code théoriquement sécurisée)
• L'apprentissage automatique aide à prévenir et à alerter les tentatives de piratage en temps réel (pensez aux gardes actifs et au filtrage des spams ).
• Beaucoup plus.

Prenons l'exemple de Wired Equivalent Privacy , qui n'existe pas dans la réalité: en raison d' erreurs théoriques embarrassantes de base (pdf), le WEP est fissurable en quelques minutes.

Dans «Pourquoi les ordinateurs ne sont pas sûrs», a plaisanté Bruce Schneier

L'ingénierie de la sécurité implique la programmation de l'ordinateur de Satan.

Et l'ordinateur de Satan est difficile à tester.

Il y a beaucoup de motivation dans le monde réel pour l'étude des algorithmes de streaming provenant de la détection d'intrusion réseau. Le document ci-dessous utilise des algorithmes de streaming pour l'entropie empirique pour détecter les anomalies dans le trafic de votre réseau.

Yu Gu, Andrew McCallum et Don Towsley. Détection d'anomalies dans le trafic réseau à l'aide d'une estimation d'entropie maximale. In IMC '05: Actes de la 5e conférence ACM SIGCOMM sur la mesure Internet, pages 1–6, 2005

Contrairement aux autres réponses, il s'agit davantage de "choses dont nous devons nous inquiéter lorsque nous disons que quelque chose est" en sécurité prouvée "", par opposition aux endroits où le TCS a été utilisé en sécurité. Ainsi, il aborde la première question des problèmes de sécurité lors de l'utilisation de la théorie.

Comme le disent les pirates, les résultats théoriques sont souvent tangentiels à la sécurité du monde réel. Ce type d'argument a été rendu plus théorique, scientifique et précis par Alfred Menezes et Neal Koblitz dans leur série de documents ' Another Look ' (attention: le site me semble un peu conflictuel, mais je pense que l'idée de base de remettre en question les hypothèses c'est tres important). Ils soulignent les faiblesses des hypothèses standard en cryptographie, même dans les articles fondateurs.

Quelques exemples (citant / paraphrasant quelques points de leur site):

1. Un théorème de sécurité est conditionnel - il suppose l'intraçabilité de certains problèmes mathématiques.

2. Souvent, l'hypothèse d'intractabilité est faite pour un problème compliqué et artificiel: dans certains cas, le problème est trivialement équivalent au problème de cryptanalyse pour le protocole dont la sécurité est "prouvée".

3. Parfois, une épreuve a un grand écart d'étanchéité, mais les tailles de paramètres sont toujours recommandées comme si l'épreuve avait été étanche. Dans de tels cas, la preuve donne généralement une limite inférieure inutile sur le temps d'exécution d'une attaque réussie. En outre, un résultat asymptotique ne fournit pas nécessairement une assurance de sécurité pour les paramètres dans la plage utilisée dans la pratique.

4. Un théorème de sécurité utilise un certain modèle de sécurité. Certaines attaques - en particulier les attaques par canal latéral - sont très difficiles à modéliser, et les modèles qui ont été proposés sont terriblement inadéquats.

Les prouveurs de théorèmes ont été utilisés dans une certaine mesure pour prouver l'exactitude des logiciels, du matériel et des protocoles. Voir, par exemple, ici ou ici .

Le problème des données circulant de manière indésirable à travers les programmes (provoquant ainsi une fuite potentielle) a été modélisé théoriquement en utilisant la notion de (non) interférence; obtenez des pointeurs ici .

La décidabilité est une préoccupation centrale dans la recherche sur les langages de programmation. C'est-à-dire que beaucoup d'efforts sont investis dans la construction de langages de programmation qui n'acceptent que du code qui satisfait certaines propriétés. Les langages statiques typiques n'offrent que de faibles garanties, comme rejeter un programme si certaines méthodes n'existent pas, mais imaginez si le langage pourrait également lancer des programmes qui, par exemple, utilisent incorrectement des mutex ou tentent de lire au-delà de la fin des régions de mémoire. Il est clair que les problèmes de décidabilité arrivent rapidement (scénario le plus simple: spécifiez que votre compilateur ne doit accepter que les programmes qui se terminent), et il y a certainement des problèmes d'efficacité (le vérificateur de type ML a des cas doublement exponentiels).

Dans tous les cas, la communauté de recherche PL s'intéresse beaucoup à la sécurité (faites-vous confiance à votre navigateur pour exécuter du code étranger arbitraire?!), Et leurs questions mènent à de nombreuses questions de théorie CS classiques.