1,720,990 research outputs found
Process Calculi and the Verification of Security Protocols
No full textRecently there has been much interest towards using formal methods in the analysis of security protocols. Some recent approaches take advantage of concepts and techniques from the field of process calculi. Process calculi can be given a formal yet simple semantics, which permits rigorous definitions of such concepts as "attacker", "secrecy"" and "authentication". This feature has led to the development of solid reasoning methods and verification techniques, a few of which we outline in this paper
Processes as formal power series: A coinductive approach to denotational semantics
No full textWe characterize must testing equivalence on CSP in terms of the unique homomorphism from the Moore automaton of CSP processes to the final Moore automaton of partial formal power series over a certain semiring. The final automaton is then turned into a CSP-algebra: operators and fixpoints are defined, respectively, via behavioural differential equations and simulation relations. This structure is then shown to be preserved by the final homomorphism. As a result, we obtain a fully abstract compositional model of CSP phrased in purely set-theoretical terms
Relative privacy threats and learning from anonymized data
No full textWe consider group-based anonymization schemes, a popular approach to data publishing. This approach aims at protecting privacy of the individuals involved in a dataset, by releasing an obfuscated version of the original data, where the exact correspondence between individuals and attribute values is hidden. When publishing data about individuals, one must typically balance the learner's utility against the risk posed by an attacker, potentially targeting individuals in the dataset. Accordingly, we propose a unified Bayesian model of group-based schemes and a related MCMC methodology to learn the population parameters from an anonymized table. This allows one to analyze the risk for any individual in the dataset to be linked to a specific sensitive value, when the attacker knows the individual's nonsensitive attributes, beyond what is implied for the general population. We call this relative threat analysis. Finally, we illustrate the results obtained with the proposed methodology on a real-world dataset
On Compositional Reasoning in the Spi–Calculus
Full text linkObservational equivalences can be used to reason about the correctness of security protocols described in the spi-calculus. Unlike in CCS or in π-calculus, these equivalences do not enjoy a simple formulation in spi-calculus. The present paper aims at enriching the set of tools for reasoning on processes by providing a few equational laws for a sensible notion of spi-bisimilarity. We discuss the difficulties underlying compositional reasoning in spi-calculus and show that, in some cases and with some care, the proposed laws can be used to build compositional proofs. A selection of these laws forms the basis of a proof system that we show to be sound and complete for the strong version of bisimilarity
Fertilizer effect on the yield and terpene components from the flowerheads of Chrysanthemum boreale M. (Compositae)
No full textChrysanthemum boreale M. is an important medicinal plant that has been historically used in natural medicine and in the food industry throughout East Asia. Most flowerheads used for food are taken from the wild. However, natural sources are limited and there is not enough to meet current demand. To fulfill current and future increasing demand, cultivation systems that produce a greater amount of flowerheads with good quality and yield are required. A field experiment was conducted during the growing seasons of 2000 and 2001 to determine the effects of fertilization treatments [without fertilizer (WF), NPK fertilizer (F), NPK plus lime (FL) and NPK plus swine manure (FS)] on flowerhead yield and the content of essential oils. Fertilizer application increased both flowerheads and essential oil yields in both growing seasons. In addition, the contents of terpene, monoterpenoids and sesquiterpenoids were improved only in FL as compared with WF or F treatments. Yield ha–1 of cumambrin A, a sesquiterpene compound exhibiting blood-pressure regulating activity, was increased by all fertilization treatments, but its concentration in the flowerheads was only increased by FL treatment. Cumambrin A and calcium contents were correlated in flower parts of C. boreale M. This suggests adding calcium could increase the yields and quality of C. boreale M. In general, the correct fertility regime could increase both flowerhead production and concentration of health-promoting substances
Fertilizer effect on the yield and terpene components from the flowerheads of Chrysanthemum boreale M. (Compositae)
No full textInternational audienceChrysanthemum boreale M. is an important medicinal plant that has been historically used in natural medicine and in the food industry throughout East Asia. Most flowerheads used for food are taken from the wild. However, natural sources are limited and there is not enough to meet current demand. To fulfill current and future increasing demand, cultivation systems that produce a greater amount of flowerheads with good quality and yield are required. A field experiment was conducted during the growing seasons of 2000 and 2001 to determine the effects of fertilization treatments [without fertilizer (WF), NPK fertilizer (F), NPK plus lime (FL) and NPK plus swine manure (FS)] on flowerhead yield and the content of essential oils. Fertilizer application increased both flowerheads and essential oil yields in both growing seasons. In addition, the contents of terpene, monoterpenoids and sesquiterpenoids were improved only in FL as compared with WF or F treatments. Yield ha-1 of cumambrin A, a sesquiterpene compound exhibiting blood-pressure regulating activity, was increased by all fertilization treatments, but its concentration in the flowerheads was only increased by FL treatment. Cumambrin A and calcium contents were correlated in flower parts of C. boreale M. This suggests adding calcium could increase the yields and quality of C. boreale M. In general, the correct fertility regime could increase both flowerhead production and concentration of health-promoting substances
Approximate model counting, sparse XOR constraints and minimum distance
Full text linkThe problem of counting the number of models of a given Boolean formula has numerous applications, including computing the leakage of deterministic programs in Quantitative Information Flow. Model counting is a hard, #P-complete problem. For this reason, many approximate counters have been developed in the last decade, offering formal guarantees of confidence and accuracy. A popular approach is based on the idea of using random XOR constraints to, roughly, successively halving the solution set until no model is left: this is checked by invocations to a SAT solver. The effectiveness of this procedure hinges on the ability of the SAT solver to deal with XOR constraints, which in turn crucially depends on the length of such constraints. We study to what extent one can employ sparse, hence short, constraints, keeping guarantees of correctness. We show that the resulting bounds are closely related to the geometry of the set of models, in particular to the minimum Hamming distance between models. We evaluate our theoretical results on a few concrete formulae. Based on our findings, we finally discuss possible directions for improvements of the current state of the art in approximate model counting
CaSPiS: A Calculus of Sessions, Pipelines and Services
Full text linkService-oriented computing is calling for novel computational models and languages with well disciplined primitives for client-server interaction, structured orchestration and unexpected events handling. We present CaSPiS, a process calculus where the conceptual abstractions of sessioning and pipelining play a central role for modelling service-oriented systems. CaSPiS sessions are two-sided, uniquely named and can be nested. CaSPiS pipelines permit orchestrating the flow of data produced by different sessions. The calculus is also equipped with operators for handling (unexpected) termination of the partner's side of a session. Several examples are presented to provide evidence of the flexibility of the chosen set of primitives. One key contribution is a fully abstract encoding of Misra et al.'s orchestration language Orc. Another main result shows that in CaSPiS it is possible to program a graceful termination of nested sessions, which guarantees that no session is forced to hang forever after the loss of its partner
Output Sampling for Output Diversity in Automatic Unit Test Generation
No full textDiverse test sets are able to expose bugs that test sets generated with structural coverage techniques cannot discover. Input-diverse test set generators have been shown to be effective for this, but also have limitations: e.g., they need to be complemented with semantic information derived from the Software Under Test. We demonstrate how to drive the test set generation process with semantic information in the form of output diversity. We present the first totally automatic output sampling for output diversity unit test set generation tool, called OutGen. OutGen transforms a program into an SMT formula in bit-vector arithmetic. It then applies universal hashing in order to generate an output-based diverse set of inputs. The result offers significant diversity improvements when measured as a high output uniqueness count. It achieves this by ensuring that the test set's output probability distribution is uniform, i.e. highly diverse. The use of output sampling, as opposed to any of input sampling, CBMC, CAVM, behaviour diversity or random testing improves mutation score and bug detection by up to 4150% and 963% respectively on programs drawn from three different corpora: the R-project, SIR and CodeFlaws. OutGen test sets achieve an average mutation score of up to 92%, and 70% of the test sets detect the defect. Moreover, OutGen is the only automatic unit test generation tool that is able to detect bugs on the real number C functions from the R-project
- …
