| 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
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.
