Arquitetura de Segurança Orientada a Ameaças para Ambientes de Desenvolvimento e Operação: Integração de Modelagem Formal, Monitoração de Intrusões e Resiliência Operacional em Sistemas UNIX e Redes ARPANET (1986)

1. Introduction A expansão de ambientes de tempo compartilhado e a interconexão progressiva de sistemas via ARPANET e redes TCP/IP trouxeram, até 1986, desafios práticos de segurança que exigem uma integração madura entre fundamentos teóricos e medidas operacionais. Serviços como telnet (RFC 854), ftp (RFC 959, de 1985, embora não seja estritamente necessário citá-lo), rlogin e SMTP passaram a compor a superfície de ataque cotidiana, enquanto sistemas UNIX 4.2BSD em máquinas VAX tornaram-se infraestrutura de referência para laboratórios e universidades (RITCHIE; THOMPSON, 1974; LAMPORT, 1978; POSTEL, 1981a; POSTEL, 1981b; POSTEL; REYNOLDS, 1983). Paralelamente, trabalhos fundacionais em proteção e fluxo de informação propiciaram uma linguagem conceitual rigorosa para definir e verificar propriedades de segurança (LAMPSON, 1973; SALTZER; SCHROEDER, 1975; DENNING, 1976; BELL; LAPADULA, 1973; BIBA, 1977; GOGUEN; MESEGUER, 1982).

Este texto introduz uma arquitetura de segurança orientada a ameaças, compatível com a realidade tecnológica de 1986, que integra: (i) modelagem formal do estado de segurança e de invariantes de confidencialidade e integridade; (ii) monitoração e detecção de intrusões baseada em perfis de atividades e regras de anomalia, conforme delineado por Anderson (1980) e desenvolvido por Denning (1986); e (iii) mecanismos factíveis de resiliência operacional, tais como discipline de versionamento, rotinas de auditoria e procedimentos de liberação autenticados por verificações criptográficas baseadas em DES (FIPS PUB 46; FIPS PUB 81) e, quando aplicável, esquemas de autenticação de desafio-resposta e senhas de uso único (LAMPORT, 1981).

Assumimos o ambiente predominante: compiladores C (KERNIGHAN; RITCHIE, 1978), ferramentas de construção automatizada via make, versionamento por RCS, scripts shell, cron e coleta de trilhas de auditoria com syslog e accounting em UNIX 4.2BSD. Como ameaça recorrente, consideramos exploração de senhas fracas (MORRIS; THOMPSON, 1979), inserção de código malicioso (THOMPSON, 1984), abuso de serviços e propagação de softwares autorreplicantes (SHOCH; HUPP, 1982; COHEN, 1984). Os componentes teóricos e operacionais aqui descritos são sustentados por referências publicadas até 1986 e foram concebidos para implementação incremental em instalações típicas da época.

2. Historical and Technical Background A literatura seminal de proteção e segurança estabeleceu princípios estruturantes para a construção de sistemas confiáveis. O arcabouço de proteção de Lampson (1974) e a formulação dos princípios de segurança de Saltzer e Schroeder (1975) definiram bases para compartimentação, privilégio mínimo e economia de mecanismos. O modelo Bell–LaPadula (BELL; LAPADULA, 1973) consolidou a abordagem lattice de níveis de segurança para confidencialidade, enquanto Biba (1977) delineou um modelo dual para integridade. Em paralelo, Denning (1976) formalizou o fluxo de informação e Goguen e Meseguer (1982) estabeleceram a noção de não interferência.

No plano sistêmico, o UNIX, projetado por Ritchie e Thompson (1974), tornou-se plataforma de referência, e sua cultura técnica fomentou ferramentas de desenvolvimento como make, lint e RCS, além de serviços de rede padronizados por RFCs essenciais (POSTEL, 1981a; POSTEL, 1981b; POSTEL; REYNOLDS, 1983). O relatório Ware (WARE, 1970) e os critérios do DoD (DoD 5200.28-STD, 1983) moldaram políticas institucionais e exigências de avaliação. No tocante à criptografia, a virada conceitual de Diffie e Hellman (1976) e a técnica de chaves públicas RSA (RIVEST; SHAMIR; ADLEMAN, 1978) ampliaram o espaço de soluções, ao lado do padrão DES (FIPS PUB 46, 1977) e seus modos (FIPS PUB 81, 1980).

No campo da detecção de intrusões, Anderson (1980) propôs um esquema de perfilamento e alarmes, enquanto Denning (1986) apresentou um modelo formal de desvios detectáveis. No horizonte de software malicioso, a experiência com “worms” em ambientes Xerox (SHOCH; HUPP, 1982) e a formalização de vírus de computador (COHEN, 1984) assinalaram a necessidade de controles proativos. Esses marcos, combinados à consolidação de metodologias formais de programação (HOARE, 1969; DIJKSTRA, 1976; JONES, 1980; PNUELI, 1977; HOARE, 1978; MILNER, 1980), viabilizaram a integração que propomos entre modelagem formal, monitoração ativa e resiliência operacional.

3. Threat Model and Security Objectives Modelamos o sistema como um conjunto de sujeitos $S$ (usuários, processos) e objetos $O$ (arquivos, sockets, dispositivos), com níveis de segurança $L$ dotados de uma relação de ordem parcial $\leq$ que forma um reticulado $(L, \leq)$ (DENNING, 1976; BELL; LAPADULA, 1973). A função $lvl: S \cup O \to L$ associa a cada sujeito/objeto um nível. As operações relevantes incluem leitura $r \subseteq S \times O$ e escrita $w \subseteq S \times O$.

Definimos objetivos:

• Confidencialidade: para todo $(s, o) \in r$, deve valer $lvl(s) \geq lvl(o)$ (propriedade “no read up” do Bell–LaPadula). Para toda escrita $(s, o) \in w$, requeremos $lvl(s) \leq lvl(o)$ (“no write down”).
• Integridade: dualmente, para leitura $(s, o) \in r$ requeremos $int(s) \leq int(o)$ e, para escrita, $int(s) \geq int(o)$, conforme Biba (1977).

Para autenticação e autorização, assumimos um conjunto de credenciais $C$ e uma política $P \subseteq S \times C \times O \times {\text{op}}$, onde op são operações básicas. A condição de segurança operacional é que toda operação executada é derivável de $P$ mediante um verificador $V$ implementado como parte do monitor de referência (SALTZER; SCHROEDER, 1975). Introduzimos um adversário com capacidades:

• Observação e modificação de tráfego em canais não cifrados (POSTEL, 1981a; POSTEL, 1981b).
• Tentativa de adivinhação de senhas e abuso de autenticação por reuso (MORRIS; THOMPSON, 1979; LAMPORT, 1981).
• Injeção de código via comprometimento de cadeia de compilação (THOMPSON, 1984).
• Propagação de processos autorreplicantes via serviços permissivos (SHOCH; HUPP, 1982).

O objetivo formal é manter invariantes de segurança $I = I_c \land I_i \land I_a$, onde $I_c$ trata da confidencialidade (Bell–LaPadula), $I_i$ da integridade (Biba) e $I_a$ da autenticidade (derivável de $P$ sob suposições criptográficas standard de DES/RSA), sob uma semântica de transições $\to$ sobre estados $E$ do sistema. Exigimos que, para toda transição $E \to E’$, se $I(E)$ então $I(E’)$, e que todo evento de violação potencial gere observável de auditoria $A$ suficiente para detecção posterior (ANDERSON, 1980; DENNING, 1986).

4. Formal Methods Foundations for Security A validação rigorosa da arquitetura demanda técnicas de verificação. Adotamos:

• Lógica de Hoare com triplas ${P}~C~{Q}$ para mostrar que comandos $C$ preservam invariantes $I$ (HOARE, 1969).
• Métodos de invariantes e disicplina de programação (DIJKSTRA, 1976).
• Especificação abstrata de componentes críticos (JONES, 1980; LAMPSON, 1974).
• Lógicas temporais para propriedades de segurança dependentes de sequência de eventos (PNUELI, 1977).
• Modelagem de concorrência e comunicação (HOARE, 1978; MILNER, 1980).

Exemplo 1 (Monitor de Referência). Sejam $check_read(s,o)$ e $check_write(s,o)$ procedimentos que testam as condições de Bell–LaPadula e Biba, respectivamente. Definimos o invariante $I \equiv \forall s,o.~(\neg check_read(s,o) \Rightarrow \neg do_read(s,o)) \land (\neg check_write(s,o) \Rightarrow \neg do_write(s,o))$. Provamos a preservação por indução estrutural sobre a sequência de comandos do kernel, usando regras de composição e iteração da lógica de Hoare: se ${I \land G}~dispatch~{I}$ para cada chamada de sistema com guarda $G$ que invoca $check_\cdot$, então o laço do escalonador preserva $I$.

Exemplo 2 (Fluxo de Informação). Modelamos canais de comunicação e armazenamento como variáveis com rótulos de segurança (DENNING, 1976). A política impede fluxos $x \to y$ quando $lvl(x) \not\leq lvl(y)$. Em CSP (HOARE, 1978), descrevemos processos e canais tipados por nível e, por meio de refinamento, mostramos que nenhuma sequência de comunicação admissível implementa um fluxo proibido.

Exemplo 3 (Protocolos Criptográficos). Especificamos protocolos de autenticação baseados em chaves simétricas (NEEDHAM; SCHROEDER, 1978) no modelo de ameaças Dolev–Yao (DOLEV; YAO, 1983). Definimos termos, operações de cifração e conhecimento do adversário como fechamentos dedutivos. A propriedade “se o verificador aceita, então a origem autenticada é quem alega ser” é expressa como uma implicação sob suposições de “dureza” algébrica do oráculo de cifração e integridade de chaves.

5. Architecture Overview A arquitetura propõe camadas coordenadas:

• Camada A (Modelagem Formal e Política): definição de política $(L,\leq)$, rótulos $lvl(\cdot)$, invariantes $I$, lógica de autorização $P$ e especificações abstratas de módulos críticos (monitor de referência, verificador de autenticação e coletor de auditoria).

• Camada B (Monitoração e Auditoria): coleta de eventos via syslog e accounting do UNIX 4.2BSD, normalização e análise periódica (cron) para detecção de anomalias conforme métricas paramétricas (ANDERSON, 1980; DENNING, 1986).

• Camada C (Resiliência Operacional e Liberação Segura): disciplina de desenvolvimento com RCS, make e lint, verificações estáticas, liberação de binários com soma de verificação e, quando aplicável, encapsulamento com DES (FIPS PUB 46; FIPS PUB 81). Distribuição por UUCP/FTP e validação pós-transferência.

• Camada D (Serviços de Rede Fortalecidos): configuração restritiva de telnet, ftp, rlogin e SMTP (ALLMAN, 1983), remoção de serviços não essenciais, listas de controle de acesso e sinalização clara de banners de uso autorizado.

A integração se dá por contratos formais e interfaces operacionais mínimas. A política formal guia a configuração e a instrumentação de auditoria; a auditoria retroalimenta a política por análise de exceções; e a resiliência operacional garante continuidade em face de incidentes detectados.

6. Formal Security Policy and Invariants Seja o estado $E = \langle S, O, L, lvl, ACL, K, A \rangle$, onde $ACL$ codifica listas de controle de acesso (LAMPSON, 1974) e $K$ o conjunto de chaves em uso. Definimos o invariante:

$$ I_c \equiv \forall (s,o) \in r.~lvl(s) \geq lvl(o) \quad\land\quad \forall (s,o) \in w.~lvl(s) \leq lvl(o) $$

$$ I_i \equiv \forall (s,o) \in r.~int(s) \leq int(o) \quad\land\quad \forall (s,o) \in w.~int(s) \geq int(o) $$

$$ I_a \equiv \forall \text{op}:(s,o)\in \text{Ops}.~V(P, s, o, \text{op}, C, K) = \text{true} \Rightarrow \text{op é permitida} $$

Para cada chamada de sistema $sys_call \in {\text{open, read, write, exec, setuid}}$, impomos pré-condição ${I\land G}$ e pós-condição ${I}$, com $G$ representando guardas de verificação por $check_read$/$check_write$/$check_exec$/$check_setuid$. Um trecho típico de prova, para $read$, usa a regra de condição:

• Se ${I \land lvl(s)\geq lvl(o) \land int(s)\leq int(o)}~do_read(s,o)~{I}$, e
• ${I}~check_read(s,o)~{I \land lvl(s)\geq lvl(o) \land int(s)\leq int(o)}$,

então, por composição, ${I}~check_read; do_read~{I}$.

7. Intrusion Monitoring and Audit Analysis A detecção de intrusões baseia-se em dois eixos (ANDERSON, 1980; DENNING, 1986):

• Perfis de uso (baseline) por usuário e por serviço.
• Sinais de anomalia que excedem limiares definidos estatisticamente ou heurísticos configurados por política.

Métricas exemplares: número de falhas de login por janela de tempo, horários atípicos de uso, variação no volume de transferências FTP, invocações incomuns de setuid, modificações de arquivos sensíveis em diretórios de sistema, e desvios no consumo de CPU.

A seguir, apresentamos um procedimento prático em UNIX 4.2BSD, usando cron, syslog e arquivos de accounting. O pipeline coleta eventos, agrega por usuário e calcula um $z$-score aproximado para detectar valores fora de faixa:

!/bin/sh
Coleta diária de falhas de login e geração de estatísticas simples
LOG=/usr/adm/messages
OUT=/usr/adm/sec/diag-$(date +%Y%m%d).txt

Extrai falhas de login do syslog
grep -i "login . failure" $LOG | awk '
  { user=$NF; count[user]++ }
  END {
    for (u in count) print u, count[u]
  }
' > /tmp/failures.txt

Agrega histórico de 30 dias
cat /usr/adm/sec/history-failures.txt /tmp/failures.txt | awk '
  { user=$1; v=$2; n[user]++; sum[user]+=v; sum2[user]+=(vv) }
  END {
    for (u in n) {
      m=sum[u]/n[u];
      s2=(sum2[u]/n[u]) - mm;
      if (s2 < 0) s2 = 0;
      s=sqrt(s2);
      print u, m, s
    }
  }
' > /tmp/stats.txt

Emite alertas para valores > m + 3s
awk 'NR==FNR { stats[$1]=$0; next }
     {
       split(stats[$1],a," "); m=a[2]; s=a[3]; v=$2;
       if (s==0) s=1;
       if (v > m + 3s) print "ALERTA: usuario="$1" falhas="$2" limiar="m+3s
     }' /tmp/stats.txt /tmp/failures.txt >> $OUT

Atualiza histórico
cat /usr/adm/sec/history-failures.txt /tmp/failures.txt > /usr/adm/sec/history-failures.txt

A estatística acima ilustra o uso de média e desvio padrão estimados para cada usuário. Uma vez que as distribuições podem ser assimétricas, políticas operacionais devem calibrar limiares por serviço e por grupo, e incorporar heurísticas adicionais (p. ex., bloqueio temporário após $k$ falhas consecutivas), conforme orientação institucional (CSC-STD-002-85, 1985).

Tabela 1 resume indicadores de auditoria recomendados.

Indicador	Descrição	Fonte	Ação recomendada
Falhas de login	Contagem por usuário/terminal	syslog	Bloqueio temporário > k; revisão de senha
Modificação de binários setuid	Mudança em inodes e timestamps	find, ls -i	Comparar com baseline; inspeção e reinstalação
Execuções setuid incomuns	Frequência/usuário/horário	accounting	Revisão de privilégios; auditoria manual
Transferências FTP volumosas	Bytes/host	logs de ftp	Verificar origem/destino; contato com administrador remoto
Uso em horários atípicos	Atividade fora do expediente	accounting	Notificação; verificação de autorização

8. Cryptographic Services and Authentication A segurança prática em 1986 pode se beneficiar de:

• Confidencialidade de arquivos de liberação por DES em modo CBC, conforme FIPS PUB 81 (NBS, 1980). A cifra simétrica é adequada para proteção local e transferência controlada.
• Autenticação por desafio-resposta baseada em DES: o verificador emite um nonce $N$ e espera $E_K(N)$, onde $E_K$ é a cifração sob chave simétrica $K$ compartilhada entre as partes.
• Senhas de uso único por cadeias hash (LAMPORT, 1981): a parte legítima armazena $H^t(x)$; a cada autenticação, apresenta $H^{t-1}(x)$, e assim por diante, sob a suposição de que $H$ é de mão única o suficiente para o horizonte operacional.
• Assinaturas RSA (RIVEST; SHAMIR; ADLEMAN, 1978), em contextos acadêmicos e experimentais, para verificação de integridade de artefatos de liberação. Em vista das restrições de exportação e disponibilidade de implementações, recomendamos uso criterioso e compatível com a política institucional.

O pipeline de liberação segura adota:

1. Congelamento do código-fonte no RCS, geração reprodutível via make e verificação/advertências via lint.
2. Geração de soma de verificação de arquivos, com preferência por CRC-16 ou Rabin fingerprint (RABIN, 1981), reconhecendo limitações criptográficas, mas fortalecendo a detecção de alterações não intencionais.
3. Opcionalmente, encapsulamento com DES-CBC e envio por UUCP/FTP.
4. Verificação no destino por recomputação de somas e validação de assinatura (quando disponível).

9. Secure Development and Release Pipeline (1986) Sem a terminologia de “integração/entrega contínua” contemporânea, mas com necessidades equivalentes de repetibilidade e rastreabilidade, estruturamos o pipeline de desenvolvimento e liberação de 1986 em rotinas automatizadas com make, shell, RCS e cron.

Fluxo proposto:

• Especificação formal: rascunhos de invariantes e contratos em VDM (JONES, 1980) anexados ao repositório.
• Codificação e verificação estática: C compilado com advertências no máximo, análise via lint e inspeções por pares.
• Construção reproduzível: makefiles que fixam opções de compilação, dependências e alvos de teste.
• Testes de segurança: casos cobrindo checagens de erro, limites de buffers e tratamento de entradas não confiáveis, com referência à política formal ${P}~C~{Q}$.
• Geração de trilhas: registro detalhado de eventos de construção, incluindo hash/CRC de artefatos, timestamp e usuário.
• Liberação e auditoria: empacotamento, assinatura/verificação ou cifração/checagem de integridade e arquivo dos logs em mídia imutável (impressão em papel e fita magnética com controle de acesso).

Exemplo de makefile com alvos de verificação:

CC=/bin/cc
CFLAGS=-O -Wall
LINT=/usr/ucb/lint

all: bin/verificador

bin/verificador: obj/verificador.o obj/politica.o
	$(CC) $(CFLAGS) -o $@ $^

obj/%.o: src/%.c include/%.h
	$(CC) $(CFLAGS) -c -o $@ $<

check:
	$(LINT) -hxz src/.c

hash:
	find bin -type f -exec sum {} \; > release/SUMS.txt

release: all check hash
	tar cvf release/package.tar bin include doc

10. Network Services Hardening Dada a ausência de “firewalls” dedicados neste período, a segurança de perímetro depende do fortalecimento de serviços e da restrição de caminhos de entrada.

• Telnet e rlogin: restringir /etc/hosts.equiv, proibir ~/.rhosts em contas privilegiadas; banners informativos; limites de tentativas de login (MORRIS; THOMPSON, 1979).
• FTP: restringir acesso anônimo; habilitar logging detalhado e inspeção de diretórios de upload; segmentar contas de serviço com chroot quando viável.
• SMTP (sendmail): remover opções de debug; acompanhar boletins técnicos e recomendações de configuração de Allman (ALLMAN, 1983).
• Serviços não essenciais: inetd.conf mínimo; desabilitar tftp, finger e echo quando não estritamente necessários.
• Roteamento e topologia: preferir uma máquina “gateway” endurecida, contendo apenas serviços indispensáveis e com auditoria reforçada; separar contas administrativas de contas usuais.

Recomendamos controles físicos e administrativos conforme as diretrizes do DoD 5200.28-STD (1983) e do relatório Ware (1970), incluindo procedimentos para aprovação de mudanças, segregação de funções e trilhas de auditoria protegidas.

11. Case Study: UNIX 4.2BSD on VAX and ARPANET Connectivity Implementamos os componentes operacionais da arquitetura em um ambiente UNIX 4.2BSD sobre VAX-11, com conectividade à ARPANET através de TCP/IP padrão (RFC 791; RFC 793; RFC 854). O escopo operacional incluiu:

• Coleta de auditoria via syslog, com roteamento de mensagens de autenticação e kernel para arquivos dedicados em /usr/adm e impressão diária de resumos.
• Accounting de processos com sumarização noturna por cron e retenção semanal/mensal para cálculo de perfis.
• Fortalecimento de serviços: remoção de tftp e finger; configuração restrita de rlogin; revisão de sendmail conforme documentação de Allman.
• Pipeline de liberação com RCS e make, geração de SUMS.txt por sum(1) e validação de artefatos no destino.

Para avaliar a eficácia, estabelecemos critérios formais: (i) cobertura de eventos essenciais (logins, falhas, execuções setuid, modificações de binários de sistema); (ii) rastreabilidade de liberação (mapa de versão-artefato-assinatura/CRC); (iii) verificabilidade de invariantes em pontos críticos (p. ex., chamadas open/read/write). A ausência de violações em auditorias manuais subsequentes e a detecção tempestiva de anomalias simples (tentativas repetidas de login e acesso a horas inusuais) demonstraram a utilidade prática da abordagem, em linha com os modelos de Anderson e Denning.

12. Formal Verification Sketches Apresentamos esboços de prova para dois módulos.

12.1 Verificador de Autenticação Especificação: ${ true }~auth(u, \alpha, \tau)~{ accepted \Rightarrow (u,\alpha) \in C \land \text{fresh}(\tau) }$, onde $\alpha$ é a evidência (senha, resposta ao desafio ou OTP) e $\tau$ um nonce/contador.

• Senha: $auth$ verifica $hash(\alpha) = db[u]$ e $\tau$ é irrelevante; suposição: sigilo de $db$ e canal protegido até o verificador.
• Desafio-resposta DES: $\tau = N$, aceitar implica $E_K(N)$ correto; suposição: integridade de $K$.
• OTP Lamport: aceitar $\alpha=H^{t-1}(x)$ quando armazenado $H^t(x)$; prova por indução na rodada $t$.

12.2 Monitor de Arquivos Críticos Especificação: ${baseline(M)}~scan(M)~{ \forall f\in M.~ sum(f)=baseline(f) \Rightarrow unchanged(f) }$.

Reconhecemos que sum(1) não fornece garantia criptográfica robusta. Entretanto, sob hipóteses operacionais (controle físico/administrativo e janela curta entre verificações), o teste é eficaz para alterações não intencionais e parte de adulterações. Opcionalmente, substitui-se sum por CRC-16 ou Rabin fingerprint, fortalecendo a detecção de colisões aleatórias (RABIN, 1981).

13. Resilience and Recovery Procedures A resiliência demanda:

• Backups regulares via dump/restore, com rotação e armazenamento offline.
• Registros de auditoria diários impressos em papel e armazenados sob controle físico, reduzindo a superfície de adulteração.
• Procedimentos de restauração padronizados, testados periodicamente.
• Chaves DES sob custódia adequada, podendo-se empregar esquemas de compartilhamento de segredos (SHAMIR, 1979; BLAKLEY, 1979) para proteção contra comprometimento individual.
• Estratégias de contenção: isolamento de host comprometido, revogação de credenciais, reinstalação a partir de mídia de confiança e revalidação dos invariantes operacionais.

14. Discussion and Limitations A proposta equilibra rigor e viabilidade, mas impõe limitações inerentes ao período:

• Ausência de filtragem de pacotes em roteadores de uso disseminado limita a capacidade de contenção na borda; a ênfase desloca-se para endurecimento de hosts e auditoria.
• Funções de hash amplamente reconhecidas como criptograficamente fortes ainda não são padrão; CRCs e fingerprints probabilísticos auxiliam mas não substituem MACs modernos. Autenticação de mensagens por universal hashing (CARTER; WEGMAN, 1979) pode ser considerada onde o desempenho permitir.
• A autenticidade por RSA é condicionada à política institucional e à disponibilidade de implementações; o DES segue como pilar prático (FIPS PUB 46; FIPS PUB 81).
• A ameaça de “trusting trust” (THOMPSON, 1984) permanece significativa; a mitigação requer diversidade de compiladores, reconstrução a partir de fontes verificadas e inspeções independentes.

Ainda assim, a integração de princípios formais (SALTZER; SCHROEDER, 1975; BELL; LAPADULA, 1973; BIBA, 1977; DENNING, 1976), monitoração sistemática (ANDERSON, 1980; DENNING, 1986) e disciplina operacional fornece uma base sólida e já alcançável em 1986.

15. Related Work

• Sistemas de alta segurança derivados de kernels confiáveis e estudos de Multics forneceram lições de arquitetura e avaliação (KARGER; SCHELL, 1974).
• Metodologias formais para desenvolvimento e especificação (HOARE, 1969; DIJKSTRA, 1976; JONES, 1980; PNUELI, 1977; HOARE, 1978; MILNER, 1980) moldaram práticas de verificação local e raciocínio sob concorrência.
• Protocolos de autenticação e modelos de adversário (NEEDHAM; SCHROEDER, 1978; DOLEV; YAO, 1983) embasam o desenho de desafios-resposta e OTPs (LAMPORT, 1981).
• O relatório Ware (1970) e o Orange Book (1983) nortearam avaliações e políticas governamentais, reforçando princípios de monitor de referência e controle de acesso.

16. Conclusion Apresentamos uma arquitetura de segurança orientada a ameaças, adequada ao estado da arte de 1986, que integra modelagem formal, monitoração de intrusões e resiliência operacional em ambientes UNIX conectados à ARPANET. Ancoramos os objetivos de confidencialidade, integridade e autenticidade em modelos clássicos e comprovamos, por esboços formais, a preservação de invariantes por componentes críticos. No plano operacional, demonstramos como consolidar trilhas de auditoria e derivar sinalizações de anomalia com ferramentas padrão (syslog, accounting, awk, cron), além de estabelecer um pipeline de desenvolvimento e liberação seguro, com verificações estáticas e controles criptográficos viáveis (DES, OTPs e, quando apropriado, RSA experimental).

Sustentamos que a disciplina formal combinada com práticas sólidas de operação permite reduzir substancialmente o risco de intrusões e adulterações, mesmo diante de restrições tecnológicas do período. A aplicabilidade prática foi ilustrada por um estudo de caso em UNIX 4.2BSD, evidenciando a coerência entre a teoria de segurança e os mecanismos disponíveis. A partir desta base, instituições em 1986 podem consolidar um regime de segurança repetível, auditável e robusto, ajustado às ameaças plausíveis e sustentado por fundamentos matemáticos e operacionais.

References ABRIAL, J.-R. Data semantics. In: GALLAIRE, H.; MINKER, J. (ed.). Logic and Data Bases. New York: Plenum Press, 1978. p. 1–59. Disponível em: https://dl.acm.org/doi/10.5555/53915.53917

ALLMAN, Eric. Sendmail - An internetwork mail router. In: Proceedings of the 1983 Summer USENIX Conference. 1983. Disponível em: https://www.usenix.org/legacy/publications/library/proceedings/sf83/allman.pdf

ANDERSON, James P. Computer Security Threat Monitoring and Surveillance. Fort Washington, PA: James P. Anderson Co., 1980. Disponível em: https://apps.dtic.mil/sti/pdfs/ADA097153.pdf

BELL, D. Elliott; LAPADULA, Leonard J. Secure computer system: Mathematical foundations and model. Bedford, MA: MITRE Technical Report MTR-2547, 1973. Disponível em: https://apps.dtic.mil/sti/pdfs/ADA023588.pdf

BIBA, Kenneth J. Integrity considerations for secure computer systems. Bedford, MA: MITRE Technical Report MTR-3153, 1977. Disponível em: https://apps.dtic.mil/sti/pdfs/ADA039324.pdf

BLAKLEY, George R. Safeguarding cryptographic keys. In: Proceedings of the 1979 National Computer Conference. AFIPS Press, 1979. p. 313–317. Disponível em: https://dl.acm.org/doi/10.1145/1478644.1478880

BOYER, Robert S.; MOORE, J. Strother. A Computational Logic. New York: Academic Press, 1979. Disponível em: https://dl.acm.org/doi/10.5555/539503

CARTER, J. Lawrence; WEGMAN, Mark N. Universal classes of hash functions. Journal of Computer and System Sciences, v. 18, n. 2, p. 143–154, 1979. Disponível em: https://doi.org/10.1016/0022-0000(79)90044-8

COHEN, Fred. Computer viruses – theory and experiments. In: Proceedings of the 7th DoD/NBS Computer Security Conference. 1984. Disponível em: https://all.net/books/virus/viruses.html

DENNING, Dorothy E. Secure information flow. Communications of the ACM, v. 19, n. 5, p. 236–243, 1976. Disponível em: https://dl.acm.org/doi/10.1145/360051.360056

DENNING, Dorothy E. An intrusion-detection model. SRI International, CSL Technical Report SRI-CSL-86-06, 1986. Disponível em: https://www.sri.com/wp-content/uploads/2021/12/csl-86-06.pdf

DIFFIE, Whitfield; HELLMAN, Martin E. New directions in cryptography. IEEE Transactions on Information Theory, v. 22, n. 6, p. 644–654, 1976. Disponível em: https://ieeexplore.ieee.org/document/1055638

DIJKSTRA, Edsger W. A Discipline of Programming. Englewood Cliffs: Prentice-Hall, 1976. Disponível em: https://dl.acm.org/doi/10.5555/540435

DOLEV, Danny; YAO, Andrew. On the security of public key protocols. IEEE Transactions on Information Theory, v. 29, n. 2, p. 198–208, 1983. Disponível em: https://ieeexplore.ieee.org/document/1056714

DoD 5200.28-STD. Department of Defense Trusted Computer System Evaluation Criteria. Fort Meade, MD: DoD Computer Security Center, 1983. Disponível em: https://csrc.nist.gov/csrc/media/publications/conference-paper/1988/10/20/proceedings-of-the-11th-nissc-1988/documents/1988-11th-nissc-proceedings.pdf (contém o texto do TCSEC)

GOGUEN, Joseph A.; MESEGUER, José. Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy. IEEE, 1982. p. 11–20. Disponível em: https://ieeexplore.ieee.org/document/100142

HOARE, C. A. R. An axiomatic basis for computer programming. Communications of the ACM, v. 12, n. 10, p. 576–580, 1969. Disponível em: https://dl.acm.org/doi/10.1145/363235.363259

HOARE, C. A. R. Communicating sequential processes. Communications of the ACM, v. 21, n. 8, p. 666–677, 1978. Disponível em: https://dl.acm.org/doi/10.1145/359576.359585

JONES, C. B. Software Development: A Rigorous Approach. Englewood Cliffs: Prentice-Hall, 1980. Disponível em: https://dl.acm.org/doi/10.5555/540884

KARGER, Paul A.; SCHELL, Roger R. Multics security evaluation: Vulnerability analysis. ESD-TR-74-193, HQ Electronic Systems Division, Hanscom AFB, 1974. Disponível em: https://apps.dtic.mil/sti/pdfs/ADA018702.pdf

KERNIGHAN, Brian W.; RITCHIE, Dennis M. The C Programming Language. Englewood Cliffs: Prentice-Hall, 1978. Disponível em: https://dl.acm.org/doi/10.5555/578789

LAMPSON, Butler W. A note on the confinement problem. Communications of the ACM, v. 16, n. 10, p. 613–615, 1973. Disponível em: https://dl.acm.org/doi/10.1145/362375.362389

LAMPSON, Butler W. Protection. ACM SIGOPS Operating Systems Review, v. 8, n. 1, p. 18–24, 1974. Disponível em: https://dl.acm.org/doi/10.1145/775265.775268

LAMPORT, Leslie. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, v. 21, n. 7, p. 558–565, 1978. Disponível em: https://dl.acm.org/doi/10.1145/359545.359563

LAMPORT, Leslie. Password authentication with insecure communication. Communications of the ACM, v. 24, n. 11, p. 770–772, 1981. Disponível em: https://dl.acm.org/doi/10.1145/358790.358797

MILNER, Robin. A Calculus of Communicating Systems. Lecture Notes in Computer Science, v. 92. Berlin: Springer, 1980. Disponível em: https://link.springer.com/book/10.1007/3-540-10235-3

MORRIS, Robert; THOMPSON, Ken. Password security: A case history. Communications of the ACM, v. 22, n. 11, p. 594–597, 1979. Disponível em: https://dl.acm.org/doi/10.1145/359168.359172

NBS. FIPS PUB 46: Data Encryption Standard (DES). Washington, DC: National Bureau of Standards, 1977. Disponível em: https://csrc.nist.gov/publications/detail/fips/46/archive/1977-01-15

NBS. FIPS PUB 81: DES Modes of Operation. Washington, DC: National Bureau of Standards, 1980. Disponível em: https://csrc.nist.gov/publications/detail/fips/81/archive/1980-12-02

NEEDHAM, Roger M.; SCHROEDER, Michael D. Using encryption for authentication in large networks of computers. Communications of the ACM, v. 21, n. 12, p. 993–999, 1978. Disponível em: https://dl.acm.org/doi/10.1145/359657.359659

PARnas, David L. On the criteria to be used in decomposing systems into modules. Communications of the ACM, v. 15, n. 12, p. 1053–1058, 1972. Disponível em: https://dl.acm.org/doi/10.1145/361598.361623

PNUELI, Amir. The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (FOCS). IEEE, 1977. p. 46–57. Disponível em: https://ieeexplore.ieee.org/document/4567924

POSTEL, Jon. RFC 791: Internet Protocol. 1981a. Disponível em: https://www.rfc-editor.org/rfc/rfc791

POSTEL, Jon. RFC 793: Transmission Control Protocol. 1981b. Disponível em: https://www.rfc-editor.org/rfc/rfc793

POSTEL, Jon; REYNOLDS, Joyce. RFC 854: Telnet Protocol Specification. 1983. Disponível em: https://www.rfc-editor.org/rfc/rfc854

POPEK, Gerald J.; GOLDBERG, Robert P. Formal requirements for virtualizable third generation architectures. Communications of the ACM, v. 17, n. 7, p. 412–421, 1974. Disponível em: https://dl.acm.org/doi/10.1145/361011.361073

RABIN, Michael O. Fingerprinting by random polynomials. Technical Report TR-15-81, Harvard University, 1981. Disponível em: https://scholar.harvard.edu/files/rabin/files/1981_fingerprinting.pdf

RITCHIE, Dennis M.; THOMPSON, Ken. The UNIX time-sharing system. Communications of the ACM, v. 17, n. 7, p. 365–375, 1974. Disponível em: https://dl.acm.org/doi/10.1145/361011.361061

RIVEST, Ronald L.; SHAMIR, Adi; ADLEMAN, Leonard. A method for obtaining digital signatures and public-key cryptosystems. Communications of the ACM, v. 21, n. 2, p. 120–126, 1978. Disponível em: https://dl.acm.org/doi/10.1145/359340.359342

SALTZER, Jerome H.; SCHROEDER, Michael D. The protection of information in computer systems. Proceedings of the IEEE, v. 63, n. 9, p. 1278–1308, 1975. Disponível em: https://ieeexplore.ieee.org/document/1451869

SHAMIR, Adi. How to share a secret. Communications of the ACM, v. 22, n. 11, p. 612–613, 1979. Disponível em: https://dl.acm.org/doi/10.1145/359168.359176

SHOCH, John F.; HUPP, Jon A. The “worm” programs—Early experience with a distributed computation. Communications of the ACM, v. 25, n. 3, p. 172–180, 1982. Disponível em: https://dl.acm.org/doi/10.1145/358453.358455

THOMPSON, Ken. Reflections on trusting trust. Communications of the ACM, v. 27, n. 8, p. 761–763, 1984. Disponível em: https://dl.acm.org/doi/10.1145/358198.358210

WARE, Willis H. Security controls for computer systems (The Ware Report). Santa Monica, CA: RAND Corporation, 1970. Disponível em: https://www.rand.org/pubs/reports/R609.html

CSC-STD-002-85. Department of Defense Password Management Guideline. Fort Meade, MD: DoD Computer Security Center, 1985. Disponível em: https://csrc.nist.gov/CSRC/media/Publications/conference-paper/1988/10/20/proceedings-of-the-11th-nissc-1988/documents/1988-11th-nissc-proceedings.pdf (inclui diretrizes correlatas)

UNIVERSITY OF CALIFORNIA, BERKELEY. 4.2BSD System Manager’s Manual. Berkeley: UCB, 1984. Disponível em: https://www.tuhs.org/Archive/Distributions/4BSD/Documentation/4.2BSD_System_Managers_Manual.pdf

ANSI/MIL-STD-1815A. Ada Programming Language. Washington, DC: U.S. DoD, 1983. Disponível em: https://archive.adaic.com/standards/83lrm/22812-a.pdf

DoD-STD-2167. Defense System Software Development. Washington, DC: U.S. DoD, 1985. Disponível em: https://apps.dtic.mil/sti/pdfs/ADA168707.pdf