Matemática aplicada
Modelagem, análise matemática e métodos computacionais para investigar problemas complexos de engenharia.
Advanced Research & Engineering
Where Mathematics Meets Engineering.
A tecnologia evolui. A complexidade aumenta. A confiança precisa ser demonstrada. Pesquisa científica e engenharia avançada para os desafios que exigem mais do que suposições.
Research
Beyond assumptions
Formal methods
Mathematical assurance
Engineering
Evidence driven
Nossa visão
Além do que funciona.
Rumo ao que podemos demonstrar.
Em um mundo onde sistemas computacionais sustentam operações críticas, transações financeiras, infraestruturas e decisões de alto impacto, existe uma diferença fundamental entre acreditar que uma tecnologia funciona e compreender, com rigor, por que ela funciona, sob quais condições e onde pode falhar.
É nessa fronteira que nasce a FikreSekhel : um laboratório independente de pesquisa científica e engenharia avançada, dedicado a enfrentar desafios tecnológicos que exigem mais do que soluções convencionais.
Nossas competências
Ciência aplicada a problemas reais.
Combinamos pesquisa matemática, ciência da computação e engenharia para investigar sistemas, algoritmos e protocolos com rigor.
Métodos formais
Especificação de propriedades, model checking, análise de estados e investigação de contraexemplos.
Criptografia
Pesquisa e análise de implementações, protocolos e propriedades relevantes à segurança criptográfica.
Segurança e engenharia
Investigação de vulnerabilidades, falhas estruturais e comportamentos inesperados em sistemas computacionais.
Research beyond assumptions
Não acreditamos que complexidade deva ser sinônimo de incerteza.
Investigamos o que não é evidente. Questionamos o que é considerado seguro. Modelamos o que parece complexo demais para ser compreendido. E buscamos demonstrar, matematicamente, aquilo que não deveria depender apenas de suposições.
“O que podemos demonstrar sobre seu comportamento —
inclusive nas condições que ninguém previu?
”
Research & Case Studies
Research that goes Beyond Assumptions.
Investigações técnicas, modelos matemáticos e evidências experimentais produzidos em nossas linhas de pesquisa. Cada estudo apresenta seu escopo e os limites das conclusões.
RESEARCH CASE / CRYPTOGRAPHY
ECDH Domain Validation Research
Investigation of elliptic-curve point validation in the js-ecutils JavaScript cryptographic library.
Investigação da validação de pontos e condições de domínio em operações ECDH, com análise de comportamento, contraexemplos e comunicação responsável com o mantenedor.
Read Research Case
Objeto: tratamento de pontos em operações de curvas elípticas e validação de entradas.
Abordagem: análise de código, experimentação e investigação de propriedades matemáticas relevantes à implementação.
Evidências: comportamento observado em testes e comunicação com o mantenedor. O escopo das conclusões deve ser acompanhado das evidências técnicas correspondentes.
RESEARCH CASE / FORMAL VERIFICATION
AES-GCM Nonce Reuse & State Safety
Formal investigation of nonce uniqueness, counter overflow and persistence failure scenarios.
Modelagem de condições que podem levar à reutilização de nonces, incluindo contadores, particionamento de espaço e falhas de persistência.
Read Research Case
Objeto: propriedades de unicidade de nonces em modelos de geração distribuída e persistência de estado.
Abordagem: modelagem de cenários e consultas de satisfatibilidade com SMT/Z3.
Limite: resultados SAT/UNSAT se referem às hipóteses e abstrações dos modelos analisados; não constituem prova irrestrita sobre implementações de produção.
RESEARCH CASE / APPLIED MATHEMATICS
JavaScript Numerical Precision Research
Investigation of IEEE-754 precision effects in modular arithmetic implementations.
Estudo de divergências entre operações numéricas de ponto flutuante e aritmética modular exata, com contraexemplos reproduzíveis.
Read Research Case
Objeto: multiplicação modular realizada com números JavaScript sujeitos às limitações de precisão do IEEE-754.
Abordagem: comparação com aritmética inteira exata e investigação de contraexemplos.
Resultado experimental: para a = b = 134217729 e p = 97, foi observada divergência entre os resultados 48 e 49 nas implementações comparadas.
RESEARCH CASE / SOFTWARE SUPPLY CHAIN
npm Supply Chain Malware Analysis
Static investigation of suspicious package installation behavior and obfuscated execution paths.
Análise independente de artefatos suspeitos em pacotes npm, com atenção a scripts de instalação, ofuscação e comportamentos potencialmente maliciosos.
Read Research Case
Objeto: pacote body-parser-js v1.0.1, investigado como caso de cadeia de suprimentos.
Abordagem: inspeção estática de artefatos e reconstrução de caminhos de execução, sem necessidade de executar o pacote suspeito.
Limite: esta apresentação resume a linha de investigação; indicadores e conclusões completas dependem do relatório técnico e de sua revisão para divulgação.
RESEARCH CASE / APPLIED CRYPTOGRAPHY
When Encryption Is Not Authentication
A Formal Analysis of AES-CBC Integrity Guarantees in Data Migration Systems.
An independent, model-based study of deterministic AES-CBC encryption, ciphertext malleability and the distinction between confidentiality and cryptographic integrity.
Read Research Case
Research question: What security properties can be established mathematically when encrypted data is processed without cryptographic authentication?
Methodology: Mathematical modeling of CBC block operations, formal proof obligations and machine-checked verification using Lean 4 and Rocq.
Verified properties: Deterministic first-block encryption under identical inputs and predictable changes to subsequent plaintext blocks when preceding ciphertext blocks are modified.
Engineering implications: The analysis demonstrates why encryption alone does not establish data authenticity and motivates authenticated encryption in security-sensitive data workflows.
Scope: This research presentation uses generic cryptographic models and does not disclose private implementations, infrastructure, operational data or client information.
RESEARCH CASE / PARSER SECURITY
When Parsing Success Does Not Mean Complete Validation
An Empirical Investigation of ASN.1 BER/DER Parsing Differentials and Cryptographic Validation Boundaries.
An independent investigation of ASN.1 parsing semantics, non-canonical length encodings and partial buffer consumption in cryptographic software. Controlled experiments compared ASN1.js with strict DER parsing in node-forge, identifying differences between successful decoding and complete input validation.
Read Research Case
Research question: Under which conditions can successful ASN.1 BER decoding be incorrectly interpreted as complete DER validation by consuming applications?
Methodology: Construction of controlled ASN.1 TLV inputs, byte-level examination of length encodings, differential testing between ASN1.js and node-forge, and analysis of parser return offsets and unconsumed input bytes.
Experimental evidence: The input 04 81 00 22 22 22 was accepted by asn1js.fromBER() as an empty OCTET STRING, consuming 3 of 6 bytes. Strict DER parsing in node-forge rejected the input. Additional tests examined non-minimal length encodings and trailing bytes.
Validation properties: Complete consumption requires the returned offset to equal the input length. Strict DER validation additionally requires compliance with canonical DER encoding restrictions. Successful BER decoding alone does not establish either property.
Engineering implications: Applications must distinguish successful parsing from complete and canonical validation. In security-sensitive workflows, inconsistent interpretation across components may introduce validation risks when parser contracts are misunderstood.
Upstream review: The findings were reported to the ASN1.js maintainers through GitHub Issue #129. The maintainer clarified the intended BER parsing contract and closed the report as a duplicate of Issue #130, which tracks stricter validation behavior.
Scope and limitations: The research establishes reproducible parsing differences and examines their potential security implications. It does not establish an exploitable vulnerability in ASN1.js or demonstrate a security bypass in a production application.
Public research references: GitHub Issue #129 | GitHub Issue #130
Nossa abordagem
Da investigação à evidência.
Da investigação de vulnerabilidades à verificação de algoritmos, protocolos e sistemas críticos, transformamos desafios de engenharia em problemas que podem ser formalizados, analisados e submetidos a métodos rigorosos de investigação e verificação.
01 — INVESTIGATE
Investigar
Compreender o sistema, suas hipóteses, propriedades críticas e possíveis modos de falha.
02 — MODEL
Modelar
Representar comportamentos e requisitos por meio de abstrações matemáticas e modelos adequados.
03 — VERIFY
Verificar
Produzir evidências, contraexemplos ou demonstrações dentro das hipóteses e limites definidos.
Colaboração & pesquisa aplicada
Problemas difíceis exigem novas formas de pensar.
Converse conosco sobre pesquisa aplicada, engenharia avançada e verificação de propriedades críticas.