A carregar...
Publicação
Coping with the reality: adding crucial features to a typestate-oriented language
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 917.78 KB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
Detecting programming errors and vulnerabilities in software is increasingly important,
and building tools that help with this task is an area of investigation, crucial for the
industry these days. When programming in an object-oriented language, one naturally
defines stateful objects that are non-uniform, i.e., their methods’ availability depends
on their internal state. One might represent their intended usage protocol with an automaton
or a state machine. Behavioral types allow to statically check if all the code of a
program respects the usage protocol of each object.
In this thesis we present a tool that extends Java with typestate definitions. These
typestates are associated with Java classes and define the behavior of instances of those
classes, specifying the sequences of method calls allowed. This tool checks statically that
method calls happen in order, following the specified behavior.
The tool was implemented in Kotlin as a plugin for the Checker Framework. It is a
new implementation of the Mungo tool and supports prevention of null pointer errors,
state transitions depending on return values, assurance of protocol completion, droppable
states, and association of protocols with classes from the standard Java library or
from third-party libraries. Additionally, the tool integrates behavioral types with access
permissions, allowing objects to be shared in a controlled way using a language of
assertions. This language of assertions supports concepts like packing and unpacking,
including unpacking of aliases objects, and transferring of permissions between aliases.
To relieve the programmer from manually writing all the necessary assertions, the tool
implements an inference algorithm which analyzes the code statically and, given the uses
of objects, constructs all the required assertions.
A deteção de erros de programação e vulnerabilidades no software é cada vez mais importante, e a criação de ferramentas que ajudem nesta tarefa é uma área de investigação crucial para a indústria atualmente. Ao programar numa linguagem orientada a objetos, definem-se naturalmente objetos com estado que não são uniformes, ou seja, a disponibilidade dos seus métodos depende do seu estado interno. Pode-se representar o protocolo de uso pretendido com um autómato ou uma máquina de estados. Os tipos comportamentais permitem verificar estaticamente se todo o código de um programa respeita o protocolo de uso de cada objeto. Nesta tese apresentamos uma ferramenta que estende o Java com definições de typestates. Esses estão associados às classes Java e definem o comportamento das instâncias dessas classes, especificando as sequências de chamadas de métodos permitidas. Esta ferramenta verifica estaticamente se as chamadas de métodos ocorrem pela ordem correta, seguindo o comportamento especificado. A ferramenta foi implementada em Kotlin como um plugin para o Checker Framework. É uma implementação nova da ferramenta Mungo e suporta a prevenção de erros de ponteiro nulo, transições de estado dependendo de valores de retorno, asseguração da conclusão dos protocolos, objetos que podem ser «largados», e a associação de protocolos com classes da biblioteca padrão do Java ou de terceiros. Além disso, esta integra tipos comportamentais com permissões de acesso, permitindo que objetos possam ser partilhados por meio de uma linguagem de asserções. Esta linguagem de asserções oferece suporte para conceitos como packing e unpacking, incluindo unpacking de objetos partilhados, e transferência de permissões entre variáveis que apontam para o mesmo objeto. Para aliviar o programador de escrever manualmente todas as asserções necessárias, a ferramenta implementa um algoritmo de inferência que analisa o código estaticamente e, consoante os usos dos objetos, constrói todas as asserções necessárias.
A deteção de erros de programação e vulnerabilidades no software é cada vez mais importante, e a criação de ferramentas que ajudem nesta tarefa é uma área de investigação crucial para a indústria atualmente. Ao programar numa linguagem orientada a objetos, definem-se naturalmente objetos com estado que não são uniformes, ou seja, a disponibilidade dos seus métodos depende do seu estado interno. Pode-se representar o protocolo de uso pretendido com um autómato ou uma máquina de estados. Os tipos comportamentais permitem verificar estaticamente se todo o código de um programa respeita o protocolo de uso de cada objeto. Nesta tese apresentamos uma ferramenta que estende o Java com definições de typestates. Esses estão associados às classes Java e definem o comportamento das instâncias dessas classes, especificando as sequências de chamadas de métodos permitidas. Esta ferramenta verifica estaticamente se as chamadas de métodos ocorrem pela ordem correta, seguindo o comportamento especificado. A ferramenta foi implementada em Kotlin como um plugin para o Checker Framework. É uma implementação nova da ferramenta Mungo e suporta a prevenção de erros de ponteiro nulo, transições de estado dependendo de valores de retorno, asseguração da conclusão dos protocolos, objetos que podem ser «largados», e a associação de protocolos com classes da biblioteca padrão do Java ou de terceiros. Além disso, esta integra tipos comportamentais com permissões de acesso, permitindo que objetos possam ser partilhados por meio de uma linguagem de asserções. Esta linguagem de asserções oferece suporte para conceitos como packing e unpacking, incluindo unpacking de objetos partilhados, e transferência de permissões entre variáveis que apontam para o mesmo objeto. Para aliviar o programador de escrever manualmente todas as asserções necessárias, a ferramenta implementa um algoritmo de inferência que analisa o código estaticamente e, consoante os usos dos objetos, constrói todas as asserções necessárias.
Descrição
Palavras-chave
Behavioral types object-oriented programming typestates session types access permissions inference