Verificação formal de uma implementação eficiente de UTF-8

Santiago, Leonardo Ribeiro

Please use this identifier to cite or link to this item:


			http://hdl.handle.net/11422/28389

Type:	Trabalho de conclusão de graduação
Title:	Verificação formal de uma implementação eficiente de UTF-8
Author(s)/Inventor(s):	Santiago, Leonardo Ribeiro
Advisor:	Gualandi, Hugo Musso
Abstract:	O sistema de codificação Unicode é imprescindível para a comunicação global, permitindo que inúmeros idiomas utilizem a mesma representação para serializar todos os caracteres, eliminando a necessidade de conversão. Dentre todos os formatos de codificação definidos pelo consórcio Unicode, certamente o formato ubíquo é o UTF-8, pela sua retrocompatibilidade com ASCII, e capacidade de economizar bytes. Apesar de ser utilizado em mais de 98% das páginas da internet, vários problemas aparecem ao implementar programas de codificação e decodificação de UTF-8 semanticamente corretos, e múltiplas vulnerabilidades estão associadas a aceitar caracteres UTF-8 inválidos erroneamente. Assim, este trabalho utiliza verificação formal através de provadores de teoremas interativos com dois propósitos. Primeiro, será desenvolvido um conjunto de propriedades - a especificação - que são suficientes para afirmar a corretude de um codicador ou decodificador de UTF-8. Com a especificação formalizada, implementamos um codificador e decodificador, mostrando que esses respeitam todas as propriedades necessárias para que estejam corretos.
Keywords:	Verificação formal Software correto Formal verification Correct software UTF-8
Subject CNPq:	CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO
Production unit:	Instituto de Computação
Publisher:	Universidade Federal do Rio de Janeiro
Issue Date:	11-Dec-2025
Publisher country:	Brasil
Language:	por
Right access:	Acesso Aberto
Appears in Collections:	Ciência da Computação

Files in This Item:

File	Description	Size	Format
LRSantiago.pdf		357.52 kB	Adobe PDF	View/Open

Show full item record Recommend this item View Statistics

Pantheon Institutional repository