Matemática aplicada
Modelagem, análise matemática e métodos computacionais para investigar problemas complexos de engenharia.
Advanced Research & Engineering
Evidência Matemática para Decisões Críticas
Há mais de dois mil anos, a matemática aprendeu a não aceitar o que apenas parece verdadeiro: ELA DEMONSTRA. Aplicamos esse mesmo rigor aos sistemas de que empresas e pessoas dependem, para que façam exatamente o que devem, e nada além disso.
Pesquisa
Além de Suposições
Métodos Formais
Garantia Matemática
Engenharia
Orientada por Evidência
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
RESEARCH CASE / FINANCIAL SYSTEMS
When a Correct Balance Hides an Unsafe Payment
Formal Verification of Payment Workflows and Robust Cash-Flow Optimization.
A correct closing balance can hide an unsafe payment. This research lab exposed over-reservation, duplicate execution and premature release of funds, then examined how to preserve liquidity and meet payment deadlines under modeled delays.
Read Research Case
Research question: Can a payment workflow preserve accounting identities while still committing unavailable funds? And can an optimized cash-flow plan remain financially safe and meet its deadlines during execution?
Methodology: State-machine modeling in Python, symbolic analysis with Z3, bounded searches for counterexamples and an inductive safety proof for a single-order recovery model. Separate optimization models examined payment dates, credit drawdowns, repayments and timing.
Counterexamples: Controlled models exposed concurrent reservations against the same cash, duplicate payments after retries, stale responses accepted after identifier reuse and funds released while a bank outcome remained uncertain. One execution reached the correct final balance despite an earlier unsafe commitment.
Liquidity under uncertainty: An explicit financing policy was checked against all 36 combinations of two receipt dates within a six-day window. In that synthetic instance, a BRL 40,000 credit limit was sufficient; a limit one cent lower admitted a counterexample.
From days to deadlines: Intraday analysis exposed a funding gap hidden by daily closing balances. Exact interest integrals and piecewise derivatives quantified the effect of timing, while a separate robust timing model found the latest credit request compatible with a payment deadline under the specified processing and confirmation delays.
Engineering implications: Expected receipts are not confirmed cash. Retries require stable identities and a defined bank idempotency contract. Financing decisions must pass execution guards, and liquidity must be checked when funds are needed, not only at the end of the day.
Scope: Independent research using synthetic financial data and explicit assumptions. Results apply to the individual models and properties analyzed. The experiments do not constitute one end-to-end proof, a production-system audit or measured client savings.
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.
Perguntas frequentes
Entenda o trabalho. Saiba o que esperar.
Como investigamos problemas críticos, quais evidências podemos produzir e como uma colaboração é estruturada.
Que tipos de problemas a FikreSekhel investiga?
Investigamos problemas de segurança e correção em software, algoritmos, protocolos criptográficos e fluxos operacionais críticos. O ponto de partida é uma pergunta concreta sobre o comportamento do sistema.
Por exemplo: uma autorização pode ser reutilizada? Duas execuções concorrentes podem duplicar um pagamento? Uma validação aceita dados que deveria rejeitar? Uma implementação preserva a propriedade matemática da qual depende?
A escolha das técnicas depende do problema: pesquisa de vulnerabilidades, análise de código, experimentos controlados, modelagem matemática, verificação formal ou otimização.
Qual é a diferença em relação a um pentest ou uma auditoria de código?
Um pentest procura demonstrar caminhos de ataque dentro de um escopo. Uma auditoria de código examina a implementação em busca de falhas. Métodos formais permitem expressar propriedades com precisão e analisar se elas são preservadas em um modelo ou em uma representação da implementação.
Essas abordagens são complementares. Uma investigação pode combinar exploração prática, revisão de código e análise formal para compreender a causa, demonstrar o comportamento e avaliar possíveis correções.
Preciso compartilhar código-fonte ou dados de produção?
Depende da pergunta e do nível de conclusão necessário. Algumas análises podem começar com documentação, especificações, exemplos de mensagens ou modelos construídos com dados sintéticos. Outras exigem acesso ao código ou a artefatos específicos.
Definimos os acessos necessários durante o planejamento. Quando trabalhamos apenas com um modelo, deixamos explícito o que foi estabelecido sobre ele e o que ainda depende de conferir sua correspondência com o sistema real.
O que minha empresa recebe ao final do trabalho?
Os entregáveis são definidos no escopo. Podem incluir relatório técnico, evidências reproduzíveis, provas de conceito controladas, modelos formais, resultados de verificação e recomendações de engenharia.
As conclusões distinguem o que foi observado, demonstrado ou permanece em aberto. Quando aplicável, também registramos as condições de reprodução, as hipóteses utilizadas e os limites de cada resultado.
A análise garante que o sistema não possui falhas?
Não de forma irrestrita. Uma análise estabelece conclusões sobre propriedades e comportamentos específicos, dentro das hipóteses e do escopo definidos.
Uma prova sobre um modelo depende da adequação desse modelo ao sistema. Uma busca limitada a determinado número de eventos não equivale a uma prova para execuções de qualquer comprimento. Da mesma forma, não encontrar uma vulnerabilidade em testes não demonstra sua inexistência.
Nosso compromisso é apresentar o alcance da evidência com precisão, permitindo que ela sustente decisões de engenharia.
É possível analisar um sistema que já está em produção?
Sim. Podemos investigar componentes ou fluxos de um sistema existente, começando por uma propriedade crítica ou um comportamento que precisa ser esclarecido.
Conforme o escopo, a investigação pode utilizar análise estática, ambientes isolados, réplicas controladas ou modelos. Qualquer interação com produção precisa ter autorização, condições operacionais e limites previamente definidos.
Como são definidos escopo, prazo e investimento?
Começamos pelo problema: qual componente está envolvido, qual propriedade importa, quais informações estão disponíveis e qual decisão a análise precisa apoiar.
A partir disso, definimos fronteiras, acessos, metodologia, entregáveis e critérios de conclusão. Prazo e investimento dependem da complexidade, do volume de artefatos e da profundidade da investigação.
Quando há muita incerteza inicial, o trabalho pode ser dividido em etapas, com um diagnóstico delimitado antes de uma investigação mais ampla.
Como funciona a confidencialidade?
As condições de confidencialidade, acesso, armazenamento, retenção e eventual divulgação são alinhadas antes do compartilhamento de material sensível e formalizadas conforme a contratação.
A publicação de um case não deve ser presumida como parte do trabalho. Qualquer divulgação relacionada a um cliente precisa respeitar as autorizações e os limites acordados.
No contato inicial, descreva o problema em termos gerais, sem enviar senhas, chaves privadas, dados pessoais ou outros segredos.
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.