This paper formalizes the architecture of Hamilton V5, a continuous physical field transformer engineered for industrial automation. Moving beyond the discrete token-based processing of legacy models, Hamilton V5 introduces Always-On Autonomy (AOA), a paradigm that perpetually consumes raw spatiotemporal media inputs and maps them concurrently across a 12-dimensional mechanical phase space. To ensure structural stability and mitigate the compounding numerical drift common in autonomous systems, V5 integrates a closed-loop vector feedback correction mechanism. Crucially, the architecture secures high-speed hardware execution by implementing a Deterministic Proof-of-Stake Gate, which dynamically aborts actions if the predicted trajectory deviates by more than a threshold.
Open access
2 source records
Physical Unclonable Functions (PUFs) and Hardware Security
Current mobile System-on-Chip (SoC) architectures suffer from a fundamental ”Reactive Polling Tax,” where high-level software must frequently interrupt low-power hardware states to query rawsensor telemetry. This paper introduces the Contextual Neural Bus (CNB), a dedicated, asynchronous hardware-level interconnect designed to shift context awareness from volatile software cycles to deterministic silicon logic. By utilizing a decentralized multi-modal fusion layer, the CNB generates Universal Intent Tokens (UITs)—64-bit cryptographic primitives that represent verified user states at the physical layer. Unlike legacy co-processors that merely buffer data, the CNB integrates a Hardware-Resident Zero-Knowledge Proof (ZKP) Generator to provide mathematical certainty of user intentwhile physically isolating raw biometric and environmental telemetry within a secure silicon enclave. Preliminary simulations using a digital-twin SoC model indicate a 90.8% reduction in interrupt driven power consumption, effectively achieving ”Energy-Neutral Privacy” by utilizing the resulting power surplus to offset cryptographic overhead. Furthermore, the architecture introduces Predictive L3 Cache Pre-warming, which anticipates user interactions to virtually eliminate ”cold-start” application latencies. By anchoring proactive computing in the deterministic reliability of silicon, this work establishes a scalable, privacy-first path toward zero-latency, energy-autonomous mobile ecosystems.
Decentralized finance (DeFi) is an emerging financial service on blockchain, enabling automatic and anonymous transactions.Within DeFi, decentralized exchanges (DEXs) maintain reserves of a pair of tokens and determine the exchange rate to swap tokens.However, DEXs also create opportunities for Maximal Extractable Value (MEV), where attackers include, exclude, or reorder DEX transactions to exploit price discrepancies of tokens and extract profit.Uncovering MEV opportunities requires high throughput, as the 12-second block interval and the vast search space impose strict time constraints.However, existing tools suffer from low throughput, as they rely on CPU-bound execution, which is hindered by frequent state forking and slow DEX execution.In this paper, we take the first step in leveraging GPU parallel computing power to boost MEV-search throughput in arbitrage and sandwich strategies.More precisely, we compile an MEV bot into a GPU application and then launch thousands of GPU threads to search for profit in parallel.To this end, we design new solutions to address three major challenges: designing cheatcodes to simulate transactions on GPU, proposing a memory manager to reduce GPU memory usage, and designing strategyaware mutations to improve input diversity.We implement a prototype named MeVisor that runs DEXs on GPUs and searches for MEV using a parallel genetic algorithm.Evaluated on 3,941 real MEV cases from Ethereum, MeVisor achieves 3.3M-5.1Mtransactions per second, outperforming the CPU baseline by 100,000x.In a large-scale study of Q1 2025 data, MeVisor estimates MEV opportunities ranging from 2 to 14 transactions, yielding at most $1.1 million in MEV profit.
Jinfa Hong, Bohao Zhang, Gaoyu Mao, Patrick S. Y. Hung · 5 authors
Lattice-based cryptography (LBC) is an essential direction in the fields of homomorphic encryption (HE), zero-knowledge proofs (ZK), and post-quantum cryptography (PQC), while number theoretic transformations (NTT) are a performance bottleneck that affects the promotion and deployment of LBC applications. Field-programmable gate arrays (FPGAs) are an ideal platform for accelerating NTT due to their reconfigurability and parallel capabilities. High-level synthesis (HLS) can shorten the FPGA development cycle, but for algorithms such as NTT, the synthesizer struggles to handle the inherent memory dependencies, often resulting in suboptimal synthesis outcomes for direct designs. This paper proposes a systematic HLS co-design to progressively guide the synthesis of NTT accelerators. The approach integrates several key techniques: arithmetic module resource optimization, conflict-free butterfly scheduling, memory partitioning, and template-based automated design fusion. It reveals how to resolve pipeline bottlenecks in HLS-based designs and expand parallel processing, guiding microarchitecture iterations to achieve an efficient design space. Compared to existing HLS-based designs, the area-latency product achieves a performance improvement of 1.93 to 191 times, and compared to existing HDL-based designs, the area-cycle product achieves a performance improvement of 1.7 to 10.6 times.
Web Assembly (Wasm) and blockchain technology offer a viable solution for reliable and high-performance front-end systems. Wasm provides high execution speeds by incorporating code from high-level languages to improvise on performance limitations. Its sand-boxed execution model enhances security by extenuating memory-related weaknesses. Similarly, blockchain reinforces security with decentralized, tamper-resistant data structures and smart contracts. Conventional blockchain frameworks often suffer from computational overhead, but Wasm-based execution platforms like Polkadot and EOS optimize resource utilization and improve interoperability. This integration facilitates high-speed, reliable interactions in decentralized applications (dApps). Potential benefits include fast and secure off-chain computations, hence reducing blockchain congestion in front-end frameworks. However, challenges remain in securing Wasm execution in decentralized environments and optimizing blockchain and Wasm interoperability. A promising direction is to exploit Just-In-Time (JIT), Ahead-of-Time (AOT) compilation schemes along with zero-knowledge proofs to further enhance performance and security characteristics. By coupling Wasm’s efficiency with blockchain’s security, scalable and decentralized front-end systems are evolving to meet challenging web demand scenarios.
Abstract- The evolution of blockchain and Web3 technologies has paved the way for decentralized application platforms that enable transparent, tamper-proof transactions without relying on centralized servers. However, existing solutions such as Gitcoin and Giveth are either too complex or unsuitable for modular deployment in educational and lightweight environments. This paper proposes MetaSuite, a role-based, blockchain-driven Software-as-a-Service (SaaS) platform that enables users to create, transfer, and donate tokens while allowing an administrator to securely withdraw funds. Built entirely on the Ethereum blockchain using Solidity smart contracts, MetaSuite operates without a backend and integrates wallet-based authentication via MetaMask and Ethers.js. The platform ensures transparent fund management through on-chain event logging and role-based access controls. Performance evaluations on the Ethereum HoleskyTestnet demonstrate the system’s reliability, gas-efficiency, and real-time responsiveness. By eliminating backend dependencies and emphasizing traceability, MetaSuite serves as a minimalistic yet scalable Web3 solution suitable for academic, experimental, and small-scale real-world deployments. Keywords—Blockchain, Web3, Smart Contracts, Ethereum, MetaMask, Tokenization, SaaS, Ethers.js, Decentralized Applications.
Multi-scalar multiplication (MSM) is the primary building block in many pairing-based zero-knowledge proof (ZKP) systems. MSM at large scales has become the main bottleneck in ZKP implementations. Inspired by existing SIMD-accelerated work, we are focused on accelerating MSM computing efficiency using SIMD instructions in a single CPU environment. First, we propose a SIMD-accelerated MSM computing architecture with no write conflicts and constant memory overheads. This architecture utilizes multithreading to achieve task-level and loop-level parallelism and employs a three-tier buffer mechanism to maximize the utilization of the SIMD engine. Instanced with AVX512-IFMA instructions, we implement six SIMD elliptic curve arithmetic engines for different point addition in three coordinate systems and two groups. Moreover, we integrate our AVX-MSM implementation into the libsnark library, naming it AVX-ZK. In more detail, point deduplication and “Three-Stage” memory optimization are proposed to address problems existing in practical applications. Based on the RELIC library, our performance results on the BLS12-381 curve show that our AVX-MSM achieves up to 27.86x speedup over the most popular Pippenger algorithm. Compared with libsnark, our AVX-ZK implementation achieves over 11.53x (up to 20.26x) speedup under standard benchmarks.
Federated Learning (FL) is a widespread approach that allows training machine learning (ML) models with data distributed across multiple devices. In cross-silo FL, which often appears in domains like healthcare or finance, the number of participants is moderate, and each party typically represents a well-known organization. For instance, in medicine data owners are often hospitals or data hubs which are well-established entities. However, malicious parties may still attempt to disturb the training procedure in order to obtain certain benefits, for example, a biased result or a reduction in computational load. While one can easily detect a malicious agent when data used for training is public, the problem becomes much more acute when it is necessary to maintain the privacy of the training dataset. To address this issue, there is recently growing interest in developing verifiable protocols, where one can check that parties do not deviate from the training procedure and perform computations correctly. In this paper, we present a systematization of knowledge on verifiable cross-silo FL. We analyze various protocols, fit them in a taxonomy, and compare their efficiency and threat models. We also analyze Zero-Knowledge Proof (ZKP) schemes and discuss how their overall cost in a FL context can be minimized. Lastly, we identify research gaps and discuss potential directions for future scientific work.
A niche corner of the Web3 world is increasingly making use of hardware-based Trusted Execution Environments (TEEs) to build decentralized infrastructure. One of the motivations to use TEEs is to go beyond the current performance limitations of cryptography-based alternatives such as zero-knowledge proofs (ZKP), fully homomorphic encryption (FHE), and multi-party computation (MPC). Despite their appealing advantages, current TEEs suffer from serious limitations as they are not secure against physical attacks, and their attestation mechanism is rooted in the chip manufacturer's trust. As a result, Web3 applications have to rely on cloud infrastruture to act as trusted guardians of hardware-based TEEs and have to accept to trust chip manufacturers. This work aims at exploring how we could potentially architect and implement chips that would be secure against physical attacks and would not require putting trust in chip manufacturers. One goal of this work is to motivate the Web3 movement to acknowledge and leverage the substantial amount of relevant hardware research that already exists. In brief, a combination of: (1) physical unclonable functions (PUFs) to secure the root-of-trust; (2) masking and redundancy techniques to secure computations; (3) open source hardware and imaging techniques to verify that a chip matches its expected design; can help move towards attesting that a given TEE can be trusted without the need to trust a cloud provider and a chip manufacturer.
Alexandr Kuznetsov, Emanuele Frontoni, Alexandr Kuznetsov, Ruslan Shevchuk · 5 authors
In the rapidly evolving field of digital asset management, centralized and decentralized global registries have become essential tools for organizing, tracking, and distributing digital assets. However, existing systems often face challenges regarding security, censorship resistance, interoperability, customizability, and scalability. This research paper aims to address these gaps by proposing a novel decentralized global registry system based on blockchain technology and non-fungible tokens (NFTs). The research paper makes several key contributions to the field of digital asset management. First, it provides a detailed system design for the proposed decentralized global registry, outlining its architectural components, functional modules, and integration with blockchain and NFT technologies. Second, it offers a thorough comparative analysis of the advantages and limitations of the proposed system in relation to existing centralized and decentralized registries. Finally, the paper presents potential use cases and practical applications of the proposed system in various industries, demonstrating its versatility and adaptability to different contexts and requirements. In conclusion, this research paper contributes significantly to the ongoing efforts to improve digital asset management by presenting a novel, decentralized global registry system based on blockchain technology and NFTs. The proposed system addresses the key limitations of existing solutions and offers a promising direction for future research and development in this critical field.
Amal Abdulbaqi Maryoosh, Ahmed Abd Ali Abdulkadhim, Muntaha AbdulzahraHatem
Block chain is a technology for securely storing data in a manner that makes system changes or hacks impossible or difficult. Numerous organizations have adopted this technology, which utilizes a peer-to-peer distributed network. Using a decentralized peer-to-peer network to operate. A block chain is a collection of linked computer systems that operate as a distributed ledger of transactions. Every new transaction that happens on the block chain is copied to each participant's ledger, and each block on the chain is made up of numerous transactions. This paper aims to explain block chain technology, including its uses and difficulties.
Orestis Alpos, Christian Cachin, Simon Holmgaard Kamp, Jesper Buus Nielsen
We present simple and practical protocols for generating randomness as used by asynchronous total-order broadcast. The protocols are secure in a proof-of-stake setting with dynamically changing stake. They can be plugged into existing protocols for asynchronous total-order broadcast and will turn these into asynchronous total-order broadcast with dynamic stake. Our contribution relies on two important techniques. The paper "Random Oracles in Constantinople: Practical Asynchronous Byzantine Agreement using Cryptography" [Cachin, Kursawe, and Shoup, PODC 2000] has influenced the design of practical total-order broadcast through its use of threshold cryptography. However, it needs a setup protocol to be efficient. In a proof-of-stake setting with dynamic stake this setup would have to be continually recomputed, making the protocol impractical. The work "Asynchronous Byzantine Agreement with Subquadratic Communication" [Blum, Katz, Liu-Zhang, and Loss, TCC 2020] showed how to use an initial setup for broadcast to asymptotically efficiently generate sub-sequent setups. The protocol, however, resorted to fully homomorphic encryption and was therefore not practically efficient. We adopt their approach to the proof-of-stake setting with dynamic stake, apply it to the Constantinople paper, and remove the need for fully homomorphic encryption. This results in simple and practical proof-of-stake protocols.
Shikaku is a pencil puzzle consisting of a rectangular grid, with some cells containing a number. The player has to partition the grid into rectangles such that each rectangle contains exactly one number equal to the area of that rectangle. In this paper, we propose two physical zero-knowledge proof protocols for Shikaku using a deck of playing cards, which allow a prover to physically show that he/she knows a solution of the puzzle without revealing it. Most importantly, in our second protocol we develop a general technique to physically verify a rectangle-shaped area with a certain size in a rectangular grid, which can be used to verify other problems with similar constraints.
Despite a considerable progress in verification of random and control logic, advances in formal verification of arithmetic designs have been lagging. This can be attributed mostly to the difficulty of efficient modeling of arithmetic circuits and data paths without resorting to computationally expensive Boolean methods, such as Binary Decision Diagrams (BDDs) and Boolean Satisfiability (SAT) that require ``bit blasting'', i.e., flattening the design to a bit-level netlist. Similarly, approaches that rely on computer algebra and Satisfiability Modulo Theories (SMT) methods are either too abstract to handle the bit-level complexity of arithmetic designs or require solving computationally expensive decision or satisfiability problems. On the other hand, theorem provers, popular solvers used in industry, require a significant human interaction and intimate knowledge of the design to guide the proof process. The work proposed in this thesis aims at overcoming the limitations of verifying arithmetic circuits, especially at the post-synthesis, implementation phase. It addresses the verification problem at an algebraic level, treating an arithmetic circuit and its specification as an algebraic system. Specifically, verification approach employed in this work is based on the algebraic rewriting method. In this method, the circuit is modeled in the algebraic domain, where both the circuit specification and its gate-level implementation are represented as polynomials. This work formally analyzes the algebraic approach and compares it with the established computer algebra methods based on Grobner basis reduction. It shows that algebraic rewriting is more effective than the Grobner basis reduction from the computational point of view. This thesis addresses two classes of arithmetic circuits that could not directly benefit from this type of functional verification, since performing algebraic rewriting of such circuits encounters a serious memory issue. The circuits that fall in the first category are approximate arithmetic circuits, such as truncated integer multipliers. Different truncation schemes are considered, including bit deletion, bit truncation, and rounding. The proposed verification method is based on reconstructing the truncated multiplier to a complete, exact multiplier; it is then followed by algebraic rewriting to prove that it indeed implements multiplication over the required range of bits. The reconstruction of the multiplier helps avoid the memory overload issue as it creates a "clean" multiplier with a well defined specification polynomial. The other class of circuits that suffer from memory overload during algebraic rewriting are circuits subjected to some arithmetic constraints. An example of such circuits is a divider, where the divisor value cannot be zero. The other example can be found in the basic blocks of the constant divider, where the value of carry into each block must be less than the divisor value. In general, such constraints will be modeled using the concept of vanishing monomials. A case-splitting method is proposed along with the modified algebraic rewriting to resolve the memory issue. The proposed verification method not only can prove that the circuit performs a correct function under the desired (valid) conditions, but also will test all the undesired (invalid) cases. This work also addresses logic debugging of combinational arithmetic circuits over field F<sub>2<sup>k</sup></sub> , including Galois field multipliers. Galois Field (GF) arithmetic has numerous applications in digital communication, cryptography and security engineering, and formal verification of such circuits is of prime importance. In addition to functional verification of GF multipliers, this work proposes a novel and effective method for identifying and correcting bugs in such circuits, commonly referred to as debugging. In this work we propose a novel approach to debugging of GF arithmetic circuits based on forward rewriting, which enables functional verification and debugging at the same time. This technique can handle multiple bugs, does not suffer from the polynomial size explosion encountered by other methods, and allows one to identify and automatically correct bugs in GF circuits. The techniques and algorithms proposed in this dissertation have been implemented in several computer programs, some stand-alone, and some integrated with a popular synthesis and verification tool, ABC. The experimental results for verification and debugging are compared with the state-of-the-art SAT, SMT, and other computer algebraic solvers.
The Android platform is undoubtedly the most popular platform for smartphones, with thousands of new applications becoming available daily and billions of app installations each year. Ethereum is the most popular smart contract platform, with thousands of applications on the blockchain serving as trading platforms and providing other functionalities. Due to these platforms’ popularity, security issues in their applications may reach a catastrophic scale with ease. Several prominent automated techniques help to reveal security problems in applications at the early stages of expansion. One such technique is static analysis. This thesis focuses on the design of static analysis techniques for Android apps and smart contracts distributed in the form of low-level code (bytecode).After installation, an Android app may get access to a set of sensitive information sources (e.g., location data). Unfortunately, exposure of such information to third parties has led in the past to several cases of privacy breach, and continues to be a serious threat. In this thesis, we tackle information flow propagation in the bytecode of Android applications by sound Horn-clause based abstraction techniques. This work will be the first to use Horn-clause based techniques in the context of security analysis. Moreover, we prove that our approach is sound, that is, our approach provides guarantees for its results. As a consequence, it can be used to show the absence of explicit data leaks in an app. Furthermore, Horn-clause based abstraction techniques are not limited to information propagation tasks, that is, our techniques can be used to show any kind of program property expressed as a reachability property. In addition, our Horn-clause based techniques scale to large codebases, benefit from the advancements in Satisfiability Modulo Theory solving, and allow for favorable performance with respect to the state-of-the-art. We instantiate the principles that were obtained while developing the analysis techniques for Android applications in the context of Ethereum smart contracts distributed in the form of Ethereum Virtual Machine (EVM) bytecode. Smart contracts are programs mainly used to perform financial operations (e.g., auctions) on cryptocurrency blockchains (e.g., Ethereum). Recent attacks demonstrate that certain vulnerabilities in smart contracts might cause severe money loss and an overall decrease of trust in the technology. Therefore, security analysis of EVM bytecode is in the focus of the research community. This thesis presents two results which establish the foundations for sound security analysis of EVM bytecode. First, the semantics of EVM bytecode is mechanized for the first time and tested against the official Ethereum test suite. This result facilitates both the design of analysis techniques and establishing their correctness properties. Second, this thesis provides the first sound Control Flow Graph reconstruction solution for EVM bytecode, that is, our analysis guarantees that reachable parts of the code are never pruned. This guarantee is required by a number of security properties for smart contracts. We also develop a tool implementing our analysis and successfully evaluate it on a big collection of real-world contracts.
This paper introduces the PoSH Consensus protocol, a novel work-in-progress construction for achieving Sybil-resistant Nakamoto-style probabilistic consensus on the contents of a cryptocurrency ledger in a permissionless decentralized network where parties stake their hardware’s computational power towards participation in leader election. PoSH aims to establish an openly mintable cryptocurrency that eliminates the requirement for block rewards and disincentivizes mining pools.
The growing use of computers in modern control systems has led to the develop- ment of complex dynamic systems known as hybrid systems, which integrates both discrete and continuous systems. Given that hybrid systems are systems that operates in real time allowing for changes in continuous state over time periods, and discrete state changes across zero time, their modelling, analysis and verification becomes very difficult. The formal verifications of such systems based on specifications that can guar- antee their behaviour is very important especially as it pertains to safety critical applications. Accordingly, addressing such verifications issues are important and is the focus of this thesis. In this thesis, in order to actualise the specification and verification of hybrid systems, Interval Temporal Logic(ITL) was adopted as the underlying formalism given its inherent characteristics of providing methods that are flexible for both propositional and first-order reasoning regarding periods found in hardware and software system’s descriptions. Given that an interval specifies the behaviour of a system, specifications of such systems are therefore represented as a set of intervals that can be used to gain an understanding of the possible behaviour of the system in terms of its composition whether in sequential or parallel form. ITL is a powerful tool that can handle both forms of composition given that it offers very strong and extensive proof and specifi- cation techniques to decipher essential system properties including safety, liveliness and time projections.However, a limitation of ITL is that the intervals within its framework are considered to be a sequence of discrete states. Against this back- drop, the current research provides an extension to ITL with the view to deal with verification and other related issues that centres around hybrid systems. The novelty within this new proposition is new logic termed SPLINE Interval Temporal Logic (SPITL) in which not only a discrete behaviour can be expressed, but also a continuous behaviour can be represented in the form of a spline i.e. the interval is considered to be a sequence of continuous phases instead of a sequence of discrete states. The syntax and semantics of the newly developed SPITL are provided in this thesis and the new extension of the interval temporal logic using a hybrid system as a case study. The overall framework adopted for the overall struc- ture of SPITL is based on three fundamental steps namely the formal specification of hybrid systems is expressed in SPLINE Interval Temporal Logic, followed by the executable subset of ITL, called Tempura, which is used to develop and test a hybrid system specification that is written in SPITL and finally a runtime verification tool for ITL called AnaTempura which is linked with Matlab in order to use them as an integrated tool for the verification of hybrid systems specification. Overall, the current work contributes to the growing body of knowledge in hybrid systems based on the following three major milestones namely: i. the proposition of a new logic termed SPITL; ii. executable subset, Tempura, integrated with SPITL specification for hybrid systems; and iii. the development of a tool termed Ana Tempura which is integrated with Matlab to ensure accurate runtime verification of results.
Modern computing platforms strive to support mobile code without putting system security at stake. These platforms can be viewed as open systems, as the mobile code adds new components to the running system. Establishing that such platforms function correctly can be divided into two steps. First, it is shown that the system functions correctly regardless of the mobile components that join it, provided that they satisfy certain assumptions. These assumptions can, for instance, restrict the behavior of the component to ensure that the security policy of the platform is not violated. Second, the mobile component is checked to satisfy its assumptions, before it is allowed to join the system. This thesis presents algorithmic verification techniques to support this methodology. In the first two parts, we present techniques for the verification of open systems relative to the given component assumptions. In the third part, a technique for the quick certification of mobile code is presented for the case where a particular type of program rewriting is used as a means of enforcing the component assumptions.In the first part of this study, we present a framework for the verification of open systems based on explicit state space representation. We propose Extended Modal Transition Systems (EMTS) as a suitable structure for representing the state space of open systems when assumptions on components are written in the modal μ-calculus. EMTSs are based on the Modal Transition Systems (MTS) of Larsen and provide a formalism for graphical specification and facilitate a thorough understanding of the system by visualization. In interactive verification, this state space representation enables proof reuse and aids the user guiding the verification process. We present a construction of state space representations from process algebraic open system descriptions based on a maximal model construction for the modal μ-calculus. The construction is sound and complete for systems with a single unknown component and sound for those without dynamic process reation. We also suggest a tableau-based proof system for establishing temporal properties of open systems represented as EMTS. The proof system is sound in general and complete for prime formulae.The problem of open system correctness also arises in compositional verification, where the problem of showing a global property of a system is reduced to showing local properties of components. In the second part, we extend an existing compositional verification framework for Java bytecode programs. The framework employs control flow graphs with procedures to model component implementations and open systems for the purpose of checking control-flow properties. We generalize these models to capture exceptional and multi-threaded behavior. The resulting control flow graphs are specifically tailored to support the compositional verification principle; however, they are sufficiently intuitive and standard to be useful on their own. We describe how the models can be extracted from program code and give preliminary experimental results for our implementation of the extraction of control flow graphs with exceptions. We also discuss further tool support and practical applications of the method.In the third part of the thesis, we develop a technique for the certification of safe mobile code, by adapting the proof-carrying code scheme of Necula to the case of security policies expressed as security automata. In particular, we describe how proofs of policy compliance can be automatically generated for programs that include a monitor for the desired policy. A monitor is an entity that observes the execution of a program and terminates the program if a violation to the property is about to occur. One way to implement such a monitor is by rewriting the program to make it self-monitoring. Given a property, we characterize self-monitoring of Java bytecode programs for this property by an annotation scheme with annotations in the style of Floyd-Hoare logics. The annotations generated by this scheme can be extended in a straightforward way to form a correctness proof in the sense of axiomatic semantics of programs. The proof generated in this manner essentially establishes that the program satisfies the property because it contains a monitor for it. The annotations that comprise the proofs are simple and efficiently checkable, thus facilitate certification of mobile code on devices with restricted computing power such as mobile phones.