To ensure that secure applications do not leak their secrets, they are required to uphold several security properties such as spatial and temporal memory safety as well as cryptographic constant time. Existing work shows how to enforce these properties individually, in an architecture-independent way, by using secure compiler passes that each focus on an individual property. Unfortunately, given two secure compiler passes that each preserve a possibly different security property, it is unclear what kind of security property is preserved by the composition of those secure compiler passes. This paper is the first to study what security properties are preserved across the composition of different secure compiler passes. Starting from a general theory of property composition for security-relevant properties (such as the aforementioned ones), this paper formalises a theory of composition of secure compilers. Then, it showcases this theory a secure multi-pass compiler that preserves the aforementioned security-relevant properties. Crucially, this paper derives the security of the multi-pass compiler from the composition of the security properties preserved by its individual passes, which include security-preserving as well as optimisation passes. From an engineering perspective, this is the desirable approach to building secure compilers.
相關內容
Economic models may exhibit incompleteness depending on whether or not they admit certain policy-relevant features such as strategic interaction, self-selection, or state dependence. We develop a novel test of model incompleteness and analyze its asymptotic properties. A key observation is that one can identify the least-favorable parametric model that represents the most challenging scenario for detecting local alternatives without knowledge of the selection mechanism. We build a robust test of incompleteness on a score function constructed from such a model. The proposed procedure remains computationally tractable even with nuisance parameters because it suffices to estimate them only under the null hypothesis of model completeness. We illustrate the test by applying it to a market entry model and a triangular model with a set-valued control function.
Variability constraints are an integral part of the requirements for a configurable system. The constraints specified in the requirements on the legal combinations of options define the space of potential valid configurations for the system-to-be. This paper reports on our experience with the variability-related requirements constraints of a flight software framework used by multiple space missions. A challenge that we saw for practitioners using the current framework, now open-sourced, is that the specifications of its variability-related requirements and constraints are dispersed across several documents, rather than being centralized in the software requirements specification. Such dispersion can contribute to misunderstandings of the side-effects of design choices, increased effort for developers, and bugs during operations. Based on our experience, we propose a new software variability model, similar to a product-line feature model, in the flight software framework. We describe the structured technique by which our model is developed, demonstrate its use, and evaluate it on a key service module of the flight software. Results show that our lightweight modeling technique helped find missing and inconsistent variability-related requirements and constraints. More generally, we suggest that a variability modeling technique such as this can be an efficient way for developers to centralize the specification and improve the analysis of dispersed variability-related requirements and constraints in other configurable systems.
Theory and application of stochastic approximation (SA) has grown within the control systems community since the earliest days of adaptive control. This paper takes a new look at the topic, motivated by recent results establishing remarkable performance of SA with (sufficiently small) constant step-size $\alpha>0$. If averaging is implemented to obtain the final parameter estimate, then the estimates are asymptotically unbiased with nearly optimal asymptotic covariance. These results have been obtained for random linear SA recursions with i.i.d.\ coefficients. This paper obtains very different conclusions in the more common case of geometrically ergodic Markovian disturbance: (i) The \textit{target bias} is identified, even in the case of non-linear SA, and is in general non-zero. The remaining results are established for linear SA recursions: (ii) the bivariate parameter-disturbance process is geometrically ergodic in a topological sense; (iii) the representation for bias has a simpler form in this case, and cannot be expected to be zero if there is multiplicative noise; (iv) the asymptotic covariance of the averaged parameters is within $O(\alpha)$ of optimal. The error term is identified, and may be massive if mean dynamics are not well conditioned. The theory is illustrated with application to TD-learning.
The aim of latent variable disentanglement is to infer the multiple informative latent representations that lie behind a data generation process and is a key factor in controllable data generation. In this paper, we propose a deep neural network-based self-supervised learning method to infer the disentangled rhythmic and harmonic representations behind music audio generation. We train a variational autoencoder that generates an audio mel-spectrogram from two latent features representing the rhythmic and harmonic content. In the training phase, the variational autoencoder is trained to reconstruct the input mel-spectrogram given its pitch-shifted version. At each forward computation in the training phase, a vector rotation operation is applied to one of the latent features, assuming that the dimensions of the feature vectors are related to pitch intervals. Therefore, in the trained variational autoencoder, the rotated latent feature represents the pitch-related information of the mel-spectrogram, and the unrotated latent feature represents the pitch-invariant information, i.e., the rhythmic content. The proposed method was evaluated using a predictor-based disentanglement metric on the learned features. Furthermore, we demonstrate its application to the automatic generation of music remixes.
In the realm of algorithmic economics, voting systems are evaluated and compared by examining the properties or axioms they satisfy. While this pursuit has yielded valuable insights, it has also led to seminal impossibility results such as Arrow's and Gibbard-Satterthwaite's Impossibility Theorems, which pose challenges in designing ideal voting systems. Enter the domain of quantum computing: recent advancements have introduced the concept of quantum voting systems, which have many potential applications including in security and blockchain. Building on recent works that bypass Arrow's Impossibility Theorem using quantum voting systems, our research extends Quantum Condorcet Voting (QCV) to counter the Gibbard-Satterthwaite Impossibility Theorem in a quantum setting. To show this, we introduce a quantum-specific notion of truthfulness, extend ideas like incentive compatibility and the purpose of onto to the quantum domain, and introduce new tools to map social welfare functions to social choice functions in this domain.
We consider outlier-robust and sparse estimation of linear regression coefficients, when the covariates and the noises are contaminated by adversarial outliers and noises are sampled from a heavy-tailed distribution. Our results present sharper error bounds under weaker assumptions than prior studies that share similar interests with this study. Our analysis relies on some sharp concentration inequalities resulting from generic chaining.
Many research explore how well computers are able to examine emotions displayed by humans and use that data to perform different tasks. However, there have been very few research which evaluate the computers ability to generate emotion classification information in an attempt to help the user make decisions or perform tasks. This is a crucial area to explore as it is paramount to the two way communication between humans and computers. This research conducted an experiment to investigate the impact of different uncertainty information displays of emotion classification on the human decision making process. Results show that displaying more uncertainty information can help users to be more confident when making decisions.
Microservices are increasingly used in modern applications, leading to a growing need for effective service integration solutions. However, we argue that traditional API-centric integration mechanisms (e.g., RPC, REST, and Pub/Sub) hamper the modularity of microservices. These mechanisms introduce rigid code-level coupling, scatter integration logic, and hinder visibility into cross-service state exchanges. Ultimately, these limitations complicate the maintenance and evolution of microservice-based applications. In response, we propose a rethinking of service integration and present Knactor, a new state-centric integration framework to restore the modularity that microservices were intended to offer. Knactor decouples service integration from service development, allowing integration to be implemented as explicit state exchanges among multiple services. Our initial case study suggests that Knactor simplifies service integration and creates new opportunities for optimizations.
Systems and blockchains often have security vulnerabilities and can be attacked by adversaries, with potentially significant negative consequences. Therefore, infrastructure providers increasingly rely on bug bounty programs, where external individuals probe the system and report any vulnerabilities (bugs) in exchange for rewards (bounty). We develop a simple contest model of bug bounty. A group of individuals of arbitrary size is invited to undertake a costly search for bugs. The individuals differ with regard to their abilities, which we capture by different costs to achieve a certain probability to find bugs if any exist. Costs are private information. We study equilibria of the contest and characterize the optimal design of bug bounty schemes. In particular, the designer can vary the size of the group of individuals invited to search, add a paid expert, insert an artificial bug with some probability, and pay multiple prizes.
What is learned by sophisticated neural network agents such as AlphaZero? This question is of both scientific and practical interest. If the representations of strong neural networks bear no resemblance to human concepts, our ability to understand faithful explanations of their decisions will be restricted, ultimately limiting what we can achieve with neural network interpretability. In this work we provide evidence that human knowledge is acquired by the AlphaZero neural network as it trains on the game of chess. By probing for a broad range of human chess concepts we show when and where these concepts are represented in the AlphaZero network. We also provide a behavioural analysis focusing on opening play, including qualitative analysis from chess Grandmaster Vladimir Kramnik. Finally, we carry out a preliminary investigation looking at the low-level details of AlphaZero's representations, and make the resulting behavioural and representational analyses available online.
小貼士
登錄享
相關主題
注冊地址： 北京市海淀區羊坊店路18號2幢3層301-191