Segurança de memória baseada em tipo sem gerenciamento manual de memória ou coleta de lixo em tempo de execução?

Digamos que queríamos uma linguagem de programação funcional, pura e funcional, como Haskell ou Idris, voltada à programação de sistemas sem coleta de lixo e sem tempo de execução (ou pelo menos não mais do que os "durações" de C e Rust). Algo que pode funcionar, mais ou menos, em metal puro.

Quais são algumas das opções de segurança da memória estática que não exigem gerenciamento manual de memória ou coleta de lixo em tempo de execução e como o problema pode ser resolvido usando o sistema de tipos de uma funcionalidade pura semelhante a Haskell ou Idris?

Grosso modo, existem duas estratégias principais para o gerenciamento seguro de memória manual.

1. A primeira abordagem é usar alguma lógica de estrutura, como a lógica linear, para controlar o uso de recursos. Essa idéia flutuou basicamente desde o início da lógica linear e basicamente trabalha com a observação de que, ao banir a regra estrutural de contração, todas as variáveis ​​são usadas no máximo uma vez e, portanto, não há alias. Como resultado, a diferença entre atualização no local e realocação é invisível para o programa e, portanto, você pode implementar seu idioma com o gerenciamento manual de memória.

   É isso que o Rust faz (usa um sistema de tipo afim). Se você está interessado na teoria das linguagens no estilo Rust, um dos melhores artigos para ler é o L3 de Ahmed et al .: A Linear Language with Locations . Além disso, o cálculo LFPL mencionado por Damiano Mazza também é linear, com uma linguagem completa derivada na linguagem RAML .

   Se você estiver interessado na verificação no estilo Idris, consulte a linguagem ATS de Xi et al. , Que é uma linguagem no estilo Rust / L3 com suporte para verificação com base nos tipos indexados no estilo Haskell, apenas tornados irrelevantes e lineares para a prova. controle sobre o desempenho.

   Uma abordagem ainda mais agressivamente dependente é a linguagem F-star desenvolvida na Microsoft Research, que é uma teoria do tipo totalmente dependente. Essa linguagem possui uma interface monádica com pré e pós-condições, no espírito da Teoria de Hoare de Nanevski et al. (Ou mesmo meus próprios tipos de integração linear e dependente ) e possui um subconjunto definido que pode ser compilado em código C de baixo nível - na verdade, eles já estão enviando código criptográfico verificado como parte do Firefox!

   Para ser claro, nem a estrela F nem o HTT são linguagens de tipo linear, mas a linguagem de índice para suas mônadas é geralmente baseada na lógica de separação de Reynold e O'Hearn , que é uma lógica de estrutura relacionada à lógica linear que teve grande sucesso como a linguagem de asserção para as lógicas Hoare para programas de ponteiro.

2. A segunda abordagem é simplesmente especificar o que a montagem (ou qualquer IR de baixo nível que você deseja) faz e, em seguida, usar alguma forma de lógica linear ou de separação para raciocinar sobre seu comportamento diretamente em um assistente de prova. Essencialmente, você pode usar o assistente de prova ou a linguagem de tipo dependente como um montador de macro muito sofisticado que gera apenas programas corretos.

   A lógica de separação de alto nível de Jensen et al para código de baixo nível é um exemplo particularmente puro disso - cria lógica de separação para montagem em x86! No entanto, existem muitos projetos nesse sentido, como o Verified Software Toolchain em Princeton e o projeto CertiKOS em Yale.

Todas essas abordagens "parecerão" um pouco com o Rust, pois acompanhar a propriedade restringindo o uso de variáveis ​​é a chave para todas elas.

Tipos lineares e lógica de separação são ótimos, mas podem exigir um pouco de esforço do programador. Escrever uma lista vinculada segura no Rust pode ser bastante difícil, por exemplo.

Mas há uma alternativa que requer muito menos esforço do programador, embora com garantias menos rigorosas. Um fluxo de trabalho (bastante antigo) é garantir a segurança da memória usando (geralmente uma pilha de) regiões. Usando a inferência de região, um compilador pode decidir estaticamente em qual região um dado de alocação deve entrar e desalocar a região quando ficar fora do escopo.

A inferência de região é comprovadamente segura (não pode desalocar memória acessível) e requer interferência mínima do programador, mas não é "total" (ou seja, ainda pode vazar memória, embora definitivamente seja muito melhor do que "não fazer nada"), por isso geralmente é combinada com GC na prática. oMLtonO compilador do ML Kit usa regiões para eliminar a maioria das chamadas de GC, mas ainda tem um GC, porque ainda assim vazaria memória. De acordo com alguns dos pioneiros em regiões, a inferência de região não foi realmente inventada para esse fim (foi para paralelização automática, eu acho); mas acabou que também poderia ser usado para gerenciamento de memória.

Como ponto de partida, eu diria que vá para o artigo "Implementação do cálculo λ de chamada por valor digitado usando uma pilha de regiões", de Mads Tofte e Jean-Pierre Talpin. Para mais artigos sobre inferência regional, procure outros trabalhos de M. Tofte e J.-P. Talpin, parte do trabalho de Pierre Jouvelot, bem como a série de artigos de Greg Morrisett, Mike Hicks e Dan Grossman sobre o Cyclone.

Um esquema trivial para os sistemas "bare metal" é simplesmente proibir todas as alocações de memória de tempo de execução. Lembre-se, mesmo o malloc/freepar C requer uma biblioteca de tempo de execução. Mas mesmo quando todos os objetos são definidos em tempo de compilação, eles podem ser definidos de maneira segura.

O principal problema aqui é a ficção de valores imutáveis ​​em linguagens funcionais puras, criadas durante a execução do programa. O hardware real (e certamente os sistemas bare metal) depende de RAM mutável, que é de suprimento limitado. Na prática, o tempo de execução de uma implementação de linguagem funcional aloca dinamicamente a RAM à medida que novos valores "imutáveis" são criados e o lixo os coleta quando o valor "imutável" não é mais necessário.

E para os problemas mais interessantes, o tempo de vida de pelo menos alguns valores depende da entrada do tempo de execução (usuário), portanto, o tempo de vida não pode ser determinado estaticamente. Mas mesmo que a vida útil não dependa de informações, pode ser altamente não trivial. Pegue o programa simples localizando repetidamente os números primos simplesmente verificando todos os números em ordem, comparando todos os números primos até sqrt(N). Claramente, essa necessidade mantém os primos e pode reciclar a memória usada para os não-primos.