Introduction

In recent decades, decentralized systems have attracted significant attention from researchers, particularly in the field of software engineering. This growing interest has led to the exploration and application of software engineering technologies in the development of efficient, secure, and reliable decentralized systems. The Software Engineering and Decentralized Systems Lab was established to bring together researchers from both fields, with the aim of advancing decentralized technologies beyond their current limitations. Our group has a strong interest in blockchain — a prominent decentralized technology — and is therefore also known as the Blockchain Lab.

Contact: dangtv@soict.hust.edu.vn (Dr. Tran Van Dang)

Research Directions

Our research interests include, but are not limited to:

1. Trust-Preserving Data Integration

• • Research question: How can data from multiple heterogeneous organizations be integrated while preserving the provenance, identity, and usage policies associated with each source?
  • Objective: Develop a trusted data model in which every data unit—even after being integrated from multiple sources—retains its provenance history, the signatures of the parties that created or transformed it, its semantic description, and its associated policies.
  • Key research areas: Representing provenance with sufficient detail for verification while remaining compact enough for efficient querying; integrating data from sources that use different schemas; verifying the integrity of an entire transformation chain; and applying semantic reasoning to connect provenance information across multiple domains.
  • Technologies and techniques: Ontologies and Semantic Web technologies, including RDF, OWL, and reasoning; provenance models based on W3C PROV; digital signatures and public key infrastructure (PKI); data integration and schema-matching techniques; and blockchain as a supporting mechanism for preventing historical records from being altered when necessary.

  Example applications:

  1. Academic credentials: Integrating degrees, transcripts, and certificates issued by multiple institutions while preserving the provenance of each source.
  2. Finance: Integrating an individual’s credit records from multiple banks and organizations while clearly identifying the source of each item and determining whether it has been modified.
  3. ESG and carbon data: Aggregating emissions data from multiple suppliers across a supply chain while retaining the origin and reporting party’s signature for each data item.

Do Ba Lam

2. Privacy-Preserving Policy Verification

• • Research question: How can an entity prove that its data satisfy a trusted policy without disclosing the original data, even when the policy and the level of trust change over time?
  • Objective: Enable the verification of complex policy statements, such as “age > 18 AND qualification = master’s degree AND issuing organization is included in the trusted list,” while ensuring that the verifier learns only that the policy has been satisfied and nothing else.
  • Key research areas: Developing a policy-representation language and mechanisms for translating policies into proof circuits; requiring input data to carry valid signatures from issuing authorities to prevent false declarations; handling time-dependent changes, including credential revocation, changes to trusted issuers, policy versioning, and proof validity at a specified point in time; and ensuring unlinkability across multiple verification sessions.
  • Technologies and techniques: Zero-knowledge proofs using Circom/snarkjs or equivalent libraries, verifiable credentials, decentralized identifiers (DIDs), digital signatures, and data structures for revocation such as accumulators and Merkle trees.

  Example applications:

  1. Academic credentials: Proving that “GPA ≥ 3.2 AND degree classification = Very Good” to a scholarship fund without disclosing the actual grades.
  2. Finance: Proving that “income meets or exceeds the loan threshold AND the applicant has no non-performing debt” to a bank without disclosing the exact income or employer—the credit eligibility problem.
  3. Digital identity: Proving that an individual is “over 18 years old AND a legal resident” to a service provider without disclosing the date of birth or address.

3. Research and Development of Verifiable Data Availability Mechanisms for Decentralized Storage Systems and Modular Blockchains

• • Research question: How can published data remain discoverable, retrievable, reconstructable, and verifiable under network churn, large-scale correlated failures, or adversarial behavior by storage nodes?
  • Objective: Develop an end-to-end mechanism that integrates erasure coding, data-shard placement, provider routing and discovery, parallel retrieval, and proofs of storage, retrieval, and repair, while jointly optimizing recovery probability, latency, and cost.
  • Key research areas:
  • 1. Erasure coding and shard placement with correlation control.
    2. Routing and provider selection under network churn and eclipse attacks.
    3. Data availability sampling and reconstruction.
    4. Cryptographic proofs of storage, retrieval, and repair.
    5. Quality-of-service and budget modeling, with evaluations conducted using prototypes and simulations.
  • Technologies and techniques: Reed–Solomon and other erasure-coding methods, distributed hash tables (DHTs), approximate nearest-neighbor search (ANNS), CRUSH-style placement mechanisms, data availability sampling, proofs of retrievability (PoR), proofs of space-time (PoSt), zero-knowledge proofs, and modular blockchains.

4. Verifiable and Poisoning-Resistant Decentralized Federated Learning

• • Research question: How can multiple organizations collaboratively train a model without sharing their original data while enabling contribution verification and limiting malicious updates in heterogeneous data environments?
  • Objective: Develop auditable, Byzantine-resilient, and privacy-preserving federated or decentralized learning protocols; quantify the trade-offs among accuracy, trustworthiness, privacy, proof-generation costs, and communication overhead.
  • Key research areas:
    1. Robust aggregation under non-independent and identically distributed (non-IID) data.
    2. Detection and isolation of model poisoning and free-riding behaviors.
    3. Verification of update validity without revealing the underlying data.
    4. Model provenance tracking and incentive mechanisms.
    5. Benchmarking in multi-organization scenarios.
  • Technologies and techniques: Federated and decentralized learning, Byzantine-robust aggregation, secure aggregation, differential privacy, verifiable computation, zero-knowledge proofs, blockchain, and distributed systems.

5. Artificial Intelligence for Formal Proof Development in Lean 4

• • Research question: How can AI be used to translate research results involving formal mathematical proofs from natural language into Lean 4 code, allowing computers to automatically verify each step of the reasoning process?
  • Objective: Develop a human–AI collaborative workflow in Lean 4 in which humans formulate definitions and theorems while AI completes the proofs in a code-generation-like process. The workflow will be evaluated using selected scientific papers.
  • Technologies and tools:
  • • Lean 4: A proof assistant used to verify mathematical proofs and critical software components. Lean originated at Microsoft Research and is currently developed by the nonprofit Lean FRO.
    • Mathlib: The largest formal mathematics library, containing more than 200,000 computer-verified theorems.
    • Large Language Models: LLMs connected directly to Lean to receive actual machine-generated feedback instead of relying on unsupported predictions.
    • Supporting tools: Semantic search within Mathlib and automated theorem-proving commands known as tactics.

  Example applications:

  1. Blockchain: Specifying and verifying decentralized finance protocols and zero-knowledge proof computation circuits.
  2. Cryptography: Proving the security properties of selected cryptographic protocols.
  3. Combinatorics and graph theory: Verifying selected theorems in combinatorics and graph theory.

6. Automated Verification and Auditing of Smart Contracts

• • Research question: Smart contracts are essential components of blockchain applications. However, errors or vulnerabilities in smart contracts can cause substantial losses after deployment. How can these errors and vulnerabilities be identified and addressed automatically?
  • Objective: Develop intelligent tools and algorithms incorporating AI to automatically verify, audit, and debug smart contracts in blockchain environments.
  • Expected results: Papers published in top-tier journals or conferences.

7. Big Data Platforms for Economics and Finance

• • Research problem: Financial data are often presented in fragmented and unstructured reports, creating a need for intelligent and scalable systems capable of collecting, processing, and storing such data.
  • Expected results: A practical application or a research paper.

8. Interoperability of Decentralized Data Management Systems

• • Research focus: Developing platforms for decentralized data interoperability while ensuring consistency across multiple systems that use heterogeneous data formats, including relational data, XML, graph data, and unstructured data.
  • Expected results: Papers published in top-tier journals or conferences.

Research Problems

Some key challenges that we are addressing include:

• Automated verification for smart contracts: Addressing the limitations of dynamic testing by leveraging static analysis to uncover bugs and vulnerabilities before deployment.
• Smart contract audit: Applying AI techniques to identify, explain, and repair bugs and vulnerabilities in smart contracts.
• Interoperability of decentralized data management systems: Developing platforms for decentralized data interoperability, ensuring consistency across multiple systems with heterogeneous data formats (relational data, XML, graph, unstructured data, etc.).
• Programming framework for maintaining data consistency: Designing programming languages for consistency-guaranteed data transformation between diverse data structures.
• Big data platform for DeFi systems: Building a big data platform for DeFi that enables real-time, multi-source data integration and analytics for financial decision support and risk management.
• Security guards for DeFi systems: Monitoring and analysing on-chain data to detect abnormal transactions and potential attacks.

Members

• Dr. Trần Văn Đặng (Head)
• Assoc. Prof. Dr. Nguyễn Bình Minh
• Dr. Đào Thành Chung
• Dr. Đỗ Bá Lâm
• Dr. Trần Vĩnh Đức
• Dr. Trịnh Tuấn Đạt
• Dr. Nguyễn Đức Anh
• Dr. Nguyễn Hữu Đức
• Assoc. Prof. Dr. Nguyễn Thị Xuân Hoà
• Assoc. Prof. Dr. Huỳnh Quyết Thắng