Making Random Choices Invisible to the Scheduler

Konstantinos Chatzikokolakis; Catuscia Palamidessi

Home/Archive/arXiv

arXiv · 0705.3503

Making Random Choices Invisible to the Scheduler

Konstantinos Chatzikokolakis·Catuscia Palamidessi

View original source ↗Read source document ↗Export metadata ↓

Abstract

When dealing with process calculi and automata which express both nondeterministic and probabilistic behavior, it is customary to introduce the notion of scheduler to solve the nondeterminism. It has been observed that for certain applications, notably those in security, the scheduler needs to be restricted so not to reveal the outcome of the protocol's random choices, or otherwise the model of adversary would be too strong even for ``obviously correct'' protocols. We propose a process-algebraic framework in which the control on the scheduler can be specified in syntactic terms, and we show how to apply it to solve the problem mentioned above. We also consider the definition of (probabilistic) may and must preorders, and we show that they are precongruences with respect to the restricted schedulers. Furthermore, we show that all the operators of the language, except replication, distribute over probabilistic summation, which is a useful property for verification.

Explore related subjects

cs.CR cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Konstantinos Chatzikokolakis, Catuscia Palamidessi. 2007-05-24. Making Random Choices Invisible to the Scheduler. https://arxiv.org/abs/0705.3503

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Bitcoin: A Non-Continuous Time System

Bitcoin has no shared global clock. Each node sees the network from its own place and at its own time. The same block may arrive at different moments, and different blocks may briefly appear at the same historical position. Yet a common history still emerges. We describe this process as a non-continuous time system (NCTS), in which the protocol state $S_h=(C_h,U_h)$ is assigned the historical coordinate $τ(S_h)=h$. This coordinate does not measure how much physical time has passed. It marks where a state belongs in the history that later states can inherit. In this framework, history advances through accepted state transitions rather than through the passage of physical time. We examine three complementary aspects of this structure. At a fixed observation point, block arrivals occur at irregular physical intervals. Across monitors, the same block is observed at different physical times. Fork data further show that competing blocks may temporarily occupy the same historical height. Taken together, these observations support the distinction between physical observation time and the historical coordinate of the inherited state sequence. The inherited past becomes increasingly stable, while the next continuation remains open to permissionless competition. Bitcoin moves forward without a shared present by inheriting a shared past.

cs.CR↗

arXiv2026

GoLeash: Mitigating Golang Software Supply Chain Attacks with Runtime Policy Enforcement

Modern software supply chain attacks consist of introducing new, malicious capabilities into trusted third-party software components, in order to propagate to a victim through a package dependency chain. These attacks are especially concerning for the Go language ecosystem, which is extensively used in critical cloud infrastructures. We present GoLeash, a novel system that applies the principle of least privilege at the package-level granularity, by enforcing distinct security policies for each package in the supply chain. This finer granularity enables GoLeash to detect malicious packages more precisely than traditional sandboxing that handles security policies at process- or container-level. Moreover, GoLeash remains effective under obfuscation, can overcome the limitations of static analysis, and incurs acceptable runtime overhead.

cs.CR↗

arXiv2026

An Empirical Analysis of EOS Blockchain: Architecture, Contract, and Security

With the rapid development of blockchain technology, various blockchain systems are exhibiting vitality and potential. As a representative of Blockchain 3.0, the EOS blockchain has been regarded as a strong competitor to Ethereum. Nevertheless, compared with Bitcoin and Ethereum, academic research and in-depth analyses of EOS remain scarce. To address this gap, this study conducts a comprehensive investigation of the EOS blockchain from five key dimensions: system architecture, decentralization, performance, smart contracts, and behavioral security. The architectural analysis focuses on six core components of the EOS system, detailing their functionalities and operational workflows. The decentralization and performance evaluations, based on data from the XBlock data-sharing platform, reveal several critical issues: low account activity, limited participation in the supernode election process, minimal variation in the set of block producers, and a substantial gap between actual throughput and the claimed million-level performance. Five types of contract vulnerabilities are identified in the smart contract dimension, and four mainstream vulnerability detection platforms are introduced and comparatively analyzed. In terms of behavioral security, four real-world attacks targeting the structural characteristics of EOS are summarized. This study contributes to the ongoing development of the EOS blockchain and provides valuable insights for enhancing the security and regulatory mechanisms of blockchain ecosystems.

cs.CR↗