map2check-sbseg2026

name	map2check-sbseg2026
description	Contexto completo do artigo SBSeg 2026 SF — Map2Check 2026. Metadados de submissão, frameworks, capítulos, backlog, restrições de edital, dados consolidados e conhecimento técnico. Ative ao trabalhar nos docs do paper.

Map2Check 2.0 — SBSeg 2026 SF

Autores: Guilherme Lucas Pereira Bernardo (UFRN), Inácio Viana (UFRN), Francisco Nobre (UFRR), Herbert Oliveira Rocha (orientador, UFRR) | Submissão: 20/jul/2026 | Sections: 5 | Single-blind — nomes podem constar

How to Use This Skill

• Without arguments — load core frameworks + submission context
• With a topic — ask about pass migration, CWE mapping, isRequired fix, WASM, backlog; I find and read the relevant chapter
• With chapter — ask for ch03; I load that specific chapter
• Browse — ask "what chapters do you have?" to see the full index

When you ask about a topic not covered below, I will read the relevant chapter file before answering.

---

📋 Submission Context (PRIORIDADE MÁXIMA)

Campo	Valor
Conferência	SBSeg 2026 — Salão de Ferramentas (SF)
Sistema de submissão	JEMS3
Idioma	Português
Deadline submissão	20/jul/2026
Notificação	03/ago/2026
Camera ready + CTA	14/ago/2026
Evento	01–04/set/2026, Armação dos Búzios — RJ
Modo	Single-blind (autores conhecidos pelos revisores — nomes/instituições/emails OK)
Template	SBC (a ser obtido)
Limite	8 pág corpo + até 2 pág referências/apêndices
Vídeo obrigatório	Sim (5-7 min) — URL pública, não precisa ser anônima
Demonstração ao vivo	Obrigatória — pelo menos 1 autor inscrito (presença CONFIRMADA)
Modalidade	Código Aberto (elegível a prêmios)
IA Generativa	Uso DECLARADO — ferramentas de IA como assistentes de escrita, conforme Código de Conduta SBC (https://sol.sbc.org.br/index.php/indice/conduta)

📝 Backlog

#	Item	Prioridade	Bloqueia	Owner
1	Referências BibTeX (TACAS 2016, 2018, 2020 + concorrentes)	Alta	Seção 2 (História) + Referências	usuário
2	Template LaTeX SBC	Alta	Geração do PDF final	usuário
3	Aprovação do orientador no outline	Alta	Sprint 1	usuário
4	WASM PoC E2E (1.7.3)	Alta	Seção WASM	✅ Concluído
5	WASM MemoryTrackPass (1.7.4)	Alta	PoC E2E	✅ Concluído
6	WASM CLI --wasm (1.7.5)	Alta	1.7.4	✅ Concluído
7	WASM Juliet benchmarks (1.7.6)	Média	1.7.5	✅ Concluído — 15 casos, 15/15 FALSE (com timeout 290s)
8	WASM seção artigo (1.7.7)	Média	1.7.6	🟡 Em andamento — texto atualizado (15/15 FALSE), figura TikZ pronta, renderização do .mmd pendente
9	Gravação do vídeo técnico	Média	Seção 5 (Demonstração)	usuário
10	Validação do build por terceiro (CTA)	Baixa	Checklist de artefato	usuário
11	Ajustes do orientador no artigo	Alta	Submissão	usuário

🛡️ CTA Checklist (Avaliação de Artefato)

Dimensão	Evidência
Disponibilidade	Repositório público + Docker image (GHCR)
Funcionalidade	Build passa + 7/7 unit tests + 9/9 passes carregando
Reprodutibilidade	Dockerfile.dev (Ubuntu 22.04) + scripts de benchmark
Sustentabilidade	CI/CD (GitHub Actions): build, unit tests, static analysis, sanitizers, e novo job E2E com Docker; docs atualizados

📊 Consolidated Data

Stack:         LLVM 16.0 · KLEE 3.1 · C++17 · Ubuntu 22.04 · Docker
Migração:      35 commits · 84 arquivos · +5.785 / -657 linhas
Unit tests:    7/7 passing
Pass plugins:  9/9 loading (opt-16)
Smoke E2E:     2/2 loops benchmarks correct (array-1.c TRUE, array-2.c FALSE)

TestComp 2026 Heap (C.coverage-error-call.Heap):
  Total:    594 tasks   | Score: 57
  TRUE:     264 (44.4%)
  UNKNOWN:  271 (45.6%)
  FALSE:     56 (9.4%) — 56 bugs reais encontrados
  FALSE(free): 1
  TIMEOUT:    2 (0.3%)
  ├─ Heap (428):        39 FALSE, 203 TRUE, 184 UNKNOWN, 2 TIMEOUT
  └─ LinkedLists (166): 18 FALSE,  61 TRUE,  87 UNKNOWN, 0 TIMEOUT

Bugs críticos corrigidos:  3 (KLEE flags, isRequired, target function)
Bugs OverflowPass corrigidos: 3 (null pointer dereference em chamadas indiretas)

TestComp 2026 ControlFlow (no-overflow):       92 tasks, 30 FALSE, 17 TRUE, 45 UNK, 0 TO (1h43m)
TestComp 2026 ControlFlow (coverage-error-call): 138 tasks, 38 FALSE, 30 TRUE, 70 UNK, 0 TO (4h53m)

WASM Pipeline:
  Branch:          feat-wasm-verification
  WABT:            1.0.41 (wasm2c)
  wasi-sdk:        33.0 (clang --target=wasm32-wasip1)
  WasmLifter:      ✅ modules/frontend/wasm_lifter.{hpp,cpp} — lifting funcional
  Entry point:     ✅ w2c_*_start → main via generateWasmWrapperStatic
  CLI --wasm:      ✅ map2check --wasm modulo.wasm — pipeline único
  WasmRuntimeStubs:✅ KLEE-friendly (calloc/free), wasm_rt_trap → map2check_error
  Wrapper auto:    ✅ generateWasmWrapperStatic() — main() → wasm bridge
  Bounds check:    ✅ Per-allocation via dlmalloc interception (w2c_*_dlmalloc/dlfree)
                   implementado e validado
  Juliet benchmarks:✅ 15 casos (CWE-121/122/124/126/127), 15/15 FALSE
                   timeout 110s → UNKNOWN; timeout 290s → FALSE
  Integration tests:✅ tests/integration/test_wasm_{pipeline,entrypoint}.sh (3/3 + 3/3)
  Seção no artigo: 🟡 Texto base em main.tex, figura pipeline pendente
  KLEE E2E:        ✅ Pipeline completo: .wasm → LLVM IR → Passes → KLEE → FALSE
  CI build:        ✅ find_path corrigido, WasmRuntimeStubs opcional
  CI E2E:          ✅ Novo job e2e-wasm executa integração dentro do Docker

🖼️ Figure Inventory

ID	Descrição	Seção	Status
fig1-timeline	Timeline visual 2016→2026	Sec 2	✅ TikZ criado (fig1-timeline.tikz.tex)
fig2-pipeline	Diagrama do pipeline de verificação (5 estágios)	Sec 3	✅ TikZ criado (fig2-pipeline.tikz.tex)
fig3-passes	Diagrama dos passes	—	Removida (orientador)
fig4-testcomp2026	Gráfico de pizza TestComp	—	Removida (orientador: nunca usar pizza)
fig5-cicd	Workflow CI/CD	—	Removida (substituída por parágrafo + OpenSSF)
fig6-wasm-pipeline	Pipeline WASM: .wasm → wasm2c → LLVM IR → Passes → KLEE	Sec 4	🟡 .mmd criado, aguardando renderização para PNG

---

Core Frameworks & Mental Models

Pipeline de Verificação Híbrida

Use fuzzing (LibFuzzer) como primeira linha para bugs superficiais — rápido mas cego para branches complexos. Use execução simbólica (KLEE) como solver de guardas quando o fuzzer estagna — preciso mas caro. A combinação (iterative deepening) resolve o trade-off.

Pass Migration Pattern (Legacy PM → New PM)

Sempre herdar de PassInfoMixin<NomeDoPass> e implementar run(Function &, FunctionAnalysisManager &). isRequired() = true é obrigatório — sem isso, opt -O0 pula o pass silenciosamente. Este foi o bug mais crítico da migração (3 bugs escaparam dos unit tests).

Mapeamento Propriedade SV-COMP → CWE → Pass

Cada propriedade de memory safety do SV-COMP mapeia para um CWE do MITRE:

• valid-free → CWE-415 (Double-Free) / CWE-416 (Use-After-Free)
• valid-deref → CWE-416 (Use-After-Free)
• valid-memsafety → CWE-119/787 (Buffer Overflow)
• valid-memcleanup → CWE-401 (Memory Leak)

O mapeamento torna resultados de verificação formal acionáveis para times de AppSec.

Modernização de Engenharia como Pré-requisito

CI/CD + Docker + static analysis + sanitizers não são luxo, são fundamento. Sem eles: bugs de regressão passam despercebidos, resultados não são reproduzíveis, a ferramenta não compete em SV-COMP/TestComp.

Docker Reproducibility Contract

Se funciona na imagem map2check-dev (Ubuntu 22.04 + LLVM 16 + KLEE 3.1), funciona em qualquer lugar. O Dockerfile.dev é o contrato de reprodutibilidade — documenta cada dependência e versão.

TestComp 2026 como Validação Empírica

Resultados Heap (594 tasks): TRUE 264 (44.4%), UNKNOWN 271 (45.6%), FALSE 56 bugs reais (9.4%), TIMEOUT 2 (0.3%). Score 57. UNKNOWN 45.6% é o principal gargalo e direciona o próximo ciclo de desenvolvimento.

UNKNOWN como KPI de Engenharia

Não é fracasso, é sinal de onde investir. Causas: timeout 300s insuficiente, path exploration do KLEE não otimizada, solver SMT (Z3) sem tuning. Cada ponto percentual reduzido de UNKNOWN é ganho real de cobertura.

Testes Unitários são Necessários mas Insuficientes

7/7 unit tests passando e 3 bugs críticos escaparam. Os bugs (KLEE flags, isRequired, target function) só foram detectados por smoke tests manuais. Testes de integração E2E (compile → instrument → link → execute) no CI são indispensáveis. No WASM, 8 commits consecutivos de "fix(ci)" tentaram fazer o CI passar sem executar KLEE; o job e2e-wasm baseado em Docker foi criado justamente para quebrar esse ciclo.

WASM como Próximo Vetor de Growth

Pipeline LLVM 16 estendido para WebAssembly. Memory safety em runtimes WASM (Wasmtime, Wasmer) é uma nova classe de bugs. Feature implementada e funcional — NÃO é trabalho futuro, aparece no paper com resultados da Juliet.

Per-Allocation Bounds Checking via dlmalloc Interception

O wasm2c gera funções de alocação com nome determinístico (w2c_dlmalloc / w2c_dlfree). O MemoryTrackPass as intercepta por padrão de nome (StringRef::contains), registrando offset + size no AllocationLog existente. Cada load/store na linear memory é verificado contra as alocações registradas via is_valid_allocation_address. Funciona para heap (malloc-based: 3/3 Juliet CWE-122/126 FALSE), não para stack/globals (CWE-121/124/127: 12/12 UNKNOWN).

Entrypoint Translation Pattern

O wasm2c traduz _start → w2c_*_start e main → w2c_*_original_main. Para unificar com o pipeline Map2Check (que espera main), geramos um wrapper C dinâmico (generateWasmWrapperStatic) que extrai o nome do módulo do entrypoint levantado, instancia o módulo WASM via wasm2c_*_instantiate, invoca _start, e libera via wasm2c_*_free. O wrapper é compilado para .bc e linkado com o IR levantado via llvm-link.

Linear Memory Bounds Gap

O bounds check nativo do wasm2c opera no nível da memória linear (0 a mem->size), não por buffer individual. Um strcpy que ultrapassa o buffer escreve no próximo byte da stack, ainda dentro dos 64KB alocados. Para detectar per-buffer overflow, é necessário rastrear limites de cada alocação — viável via dlmalloc para heap, inviável para stack/globais (Fase 2, pós-SBSeg).

Escopo do Paper — O que NÃO mencionar

• NÃO: DG Library, AFL++, Coordenador, Smart Seeds (fora do escopo — são próximos passos do pré-projeto Map2Check 2.0)
• SIM: LLVM 16, New PM, 9 passes, C++17, CI/CD, Docker, sanitizers, static analysis, TestComp 2026, CWE mapping, WASM

---

Chapter Index

#	Title	Pages	Figures	Data Sources	Key Frameworks
ch01	Introdução	~1	—	docs/paper-sbseg-2026/sbseg-article/main.tex	Memory Safety, Verificação Híbrida, CWE Top 25, Trabalhos Relacionados
ch02	História e Evolução	~1	fig1-timeline	CHANGELOG.md, docs/migration/	BMC→KLEE→Híbrido, Comparação com concorrentes (CPAchecker, Symbiotic, FuSeBMC, ESBMC)
ch03	Arquitetura e Funcionalidades	~2.5	fig2-pipeline	docs/migration/1.3-*.md, .github/workflows/, Dockerfile.dev	Pipeline 5 estágios, Técnicas (fluxo de dados, intervalos), OpenSSF
ch04	Análise Experimental	~2	—	test-comp2026/simulation/	CWE mapping, TestComp 2026 resultados, WASM lifting
[ch05]	Demonstração Planejada	—	—	—	Removida do artigo (orientador: demo não é conteúdo de paper)
ch06	Conclusão	~1	—	docs/paper-sbseg-2026/data/consolidated-data.md	Resultados, Limitações (UNKNOWN 45.6%), Perspectivas (WASM, E2E tests)

Topic Index

• AFL++ → ch01, Pré-projeto
• Arquitetura (pipeline) → ch03
• ASAN / UBSAN / TSAN → ch03, ch04
• BMC (Bounded Model Checking) → ch02
• Buffer Overflow → ch01, ch04
• C++17 → ch03
• CBMC → ch02
• Checkpoint automatizado → ch04, patterns
• CI/CD → ch03
• Crab-LLVM → ch02
• CWE-119 / 787 → ch01, ch04
• CWE-401 (Memory Leak) → ch01, ch04
• CWE-415 (Double-Free) → ch01, ch04
• CWE-416 (Use-After-Free) → ch01, ch04
• Demonstração ao vivo → ch05
• DG Library → Pré-projeto (fora do escopo paper)
• Docker → ch03, ch05
• Execução Simbólica → ch01, ch02, ch03
• FuSeBMC → ch01
• isRequired fix → ch03, ch04
• Iterative deepening → ch03, patterns
• KLEE 3.1 → ch02, ch03, ch04
• Legacy PM → New PM → ch02, ch03, patterns
• LibFuzzer → ch02, ch03
• LLVM 16 → ch03
• Memory Safety → ch01, ch04
• New Pass Manager → ch03, patterns
• OpenSSF Best Practices → ch03
• Passes (9) → ch03
• Pipeline (5 estágios) → ch03
• SBSeg SF 2026 → ch05
• Smart Seeds → ch01, Pré-projeto
• SMT Solver (Z3) → ch01, ch03
• SV-COMP → ch01
• Symbiotic → ch01
• TestComp 2026 → ch04, ch06
• UNKNOWN (45.6%) → ch04, ch06
• WASM (WebAssembly) → ch04, ch06
• WASM lifter / WABT → ch04, Implementation Plan
• wasm2c → ch04, Implementation Plan
• wasi-sdk → Implementation Plan
• w2c__start → Implementation Plan
• dlmalloc interception → ch04, patterns
• entrypoint translation → ch04, patterns
• per-allocation bounds → ch04, patterns
• linear memory gap → ch04, patterns
• Juliet Test Suite → ch04
• generateWasmWrapperStatic → ch04
• WasmRuntimeStubs → ch04
• integration tests (WASM) → tests/
• Witness GraphML → ch03

Supporting Files

• glossary.md — all key terms with definitions
• patterns.md — all techniques and design patterns
• cheatsheet.md — quick reference tables and decision guides

---

Scope & Limits

Coberto: Conteúdo do paper SBSeg 2026 SF (Map2Check modernization) + pré-projeto Map2Check 2.0 + metadados de submissão + backlog + dados consolidados de TestComp 2026.

Fora do escopo do paper (mencionados em contexto, detalhados no pré-projeto): DG Library, AFL++, Smart Seeds, Coordenador.

Fontes de referência no repo: docs/migration/ (passes, frontend, checkpoints), .github/workflows/ (CI/CD), test-comp2026/simulation/ (benchmarks), Dockerfile.dev (reprodutibilidade).

Esta skill absorveu e substitui sbseg-paper — todo o conteúdo de projeto (submissão, backlog, restrições, CTA) foi fundido aqui.