Opacidade de sistemas a eventos discretos

Motivados pela crescente necessidade de confiabilidade em diversas aplicações que requerem alguma forma de transmissão de dados, tais como sistemas de defesa, transações bancárias e até mesmo sistemas de distribuição de energia, diversas noções de segurança e privacidade foram introduzidas. Dentre essas noções, destaca-se a opacidade. De uma forma geral, a opacidade se preocupa com a caracterização do fluxo de informação do sistema para um agente externo, o intruso, e busca determinar se um comportamento secreto de um sistema é mantido opaco para “invasores” externos. Para tanto, exige-se que o intruso, aqui modelado como um observador passivo do comportamento do sistema, nunca seja capaz de determinar o real comportamento do sistema. Duas noções de opacidade são usualmente consideradas na literatura: a opacidade de linguagem e a opacidade de estados. Formalmente, para um dado mapeamento de observação, uma linguagem é fortemente opaca se todas as sequências podem ser confundidas com algumas sequências de alguma outra linguagem e é fracamente opaca se algumas sequências na linguagem são confundidas com algumas sequências na outra linguagem. Para a definição de opacidade de estados é necessário introduzir um conjunto de estados secretos S. Nesse contexto, diz-se que um sistema é opaco se, baseado em observações a partir de um mapeamento, o observador nunca estará certo se o estado atual do sistema é um dos estados secretos S. Nessa linha de pesquisa, buscamos desenvolver algoritmos em tempo polinomial para a verificação tanto da opacidade de linguagens quanto da opacidade de estados. Um outro objetivo dessa linha de pesquisa é a recuperação da opacidade, isto é, dado que um sistema seja opaco e que os mapeamentos de observação são conhecidos do proprietário do sistema, encontrar as condições necessárias e suficientes para que a opacidade não exista também para o proprietário do sistema..