| 1. |
- Cheraghchi, M., et al.
(author)
-
Approximating Linear Threshold Predicates
- 2010
-
In: Lecture Notes in Computer Science. 13th International Workshop on Approximation Algorithms for Combinatorial Optimization Problems, APPROX 2010 and 14th International Workshop on Randomization and Computation, RANDOM 2010, Barcelona, 1-3 September 2010. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 0302-9743 .- 1611-3349. - 9783642153686 ; 6302, s. 110-123
-
Conference paper (peer-reviewed)abstract
- We study constraint satisfaction problems on the domain {-1,1}, where the given constraints are homogeneous linear threshold predicates. That is, predicates of the form sgn(w1 x1+⋯+wn x n ) for some positive integer weights w 1, ..., w n . Despite their simplicity, current techniques fall short of providing a classification of these predicates in terms of approximability. In fact, it is not easy to guess whether there exists a homogeneous linear threshold predicate that is approximation resistant or not. The focus of this paper is to identify and study the approximation curve of a class of threshold predicates that allow for non-trivial approximation. Arguably the simplest such predicate is the majority predicate sgn(x 1+⋯+xn ), for which we obtain an almost complete understanding of the asymptotic approximation curve, assuming the Unique Games Conjecture. Our techniques extend to a more general class of "majority-like" predicates and we obtain parallel results for them. In order to classify these predicates, we introduce the notion of Chow-robustness that might be of independent interest.
|
|
| 2. |
- Abdelraheem, Mohamed Ahmed, et al.
(author)
-
On The Distribution of Linear Biases: Three Instructive Examples
- 2012
-
In: Lecture Notes in Computer Science : Advances in Cryptology – CRYPTO 2012 32nd Annual Cryptology Conference, Santa Barbara, CA, USA, August 19-23, 2012. Proceedings - Advances in Cryptology – CRYPTO 2012 32nd Annual Cryptology Conference, Santa Barbara, CA, USA, August 19-23, 2012. Proceedings. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 0302-9743 .- 1611-3349. - 9783642320088 - 9783642320095 ; 7417, s. 50-67
-
Conference paper (peer-reviewed)abstract
- Despite the fact that we evidently have very good block ciphers at hand today, some fundamental questions on their security are still unsolved. One such fundamental problem is to precisely assess the security of a given block cipher with respect to linear cryptanalysis. In by far most of the cases we have to make (clearly wrong) assumptions, e.g., assume independent round-keys. Besides being unsatisfactory from a scientific perspective, the lack of fundamental understanding might have an impact on the performance of the ciphers we use. As we do not understand the security sufficiently enough, we often tend to embed a security margin -- from an efficiency perspective nothing else than wasted performance. The aim of this paper is to stimulate research on these foundations of block ciphers. We do this by presenting three examples of ciphers that behave differently to what is normally assumed. Thus, on the one hand these examples serve as counter examples to common beliefs and on the other hand serve as a guideline for future work.
|
|
| 3. |
- Abed, F., et al.
(author)
-
Optimal coordination mechanisms for multi-job scheduling games
- 2014
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783662447765 ; 8737, s. 13-24
-
Conference paper (peer-reviewed)abstract
- We consider the unrelated machine scheduling game in which players control subsets of jobs. Each player's objective is to minimize the weighted sum of completion time of her jobs, while the social cost is the sum of players' costs. The goal is to design simple processing policies in the machines with small coordination ratio, i.e., the implied equilibria are within a small factor of the optimal schedule. We work with a weaker equilibrium concept that includes that of Nash. We first prove that if machines order jobs according to their processing time to weight ratio, a.k.a. Smith-rule, then the coordination ratio is at most 4, moreover this is best possible among nonpreemptive policies. Then we establish our main result. We design a preemptive policy, externality, that extends Smith-rule by adding extra delays on the jobs accounting for the negative externality they impose on other players. For this policy we prove that the coordination ratio is 1+φ≈2.618, and complement this result by proving that this ratio is best possible even if we allow for randomization or full information. Finally, we establish that this externality policy induces a potential game and that an ε-equilibrium can be found in polynomial time. An interesting consequence of our results is that an ε-local optima of R| |∑w j C j for the jump (a.k.a. move) neighborhood can be found in polynomial time and are within a factor of 2.618 of the optimal solution. The latter constitutes the first direct application of purely game-theoretic ideas to the analysis of a well studied local search heuristic.
|
|
| 4. |
- Abel, Andreas, 1974, et al.
(author)
-
A formalized proof of strong normalization for guarded recursive types
- 2014
-
In: Lecture Notes in Computer Science: 12th Asian Symposium on Programming Languages and Systems, APLAS 2014 Singapore, 17-19 November 2014. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783319127354 ; 8858, s. 140-158
-
Conference paper (peer-reviewed)abstract
- We consider a simplified version of Nakano’s guarded fixed-point types in a representation by infinite type expressions, defined coinductively. Smallstep reduction is parametrized by a natural number “depth” that expresses under how many guards we may step during evaluation. We prove that reduction is strongly normalizing for any depth. The proof involves a typed inductive notion of strong normalization and a Kripke model of types in two dimensions: depth and typing context. Our results have been formalized in Agda and serve as a case study of reasoning about a language with coinductive type expressions.
|
|
| 5. |
- Abidin, Aysajan, 1983, et al.
(author)
-
Attacks on Privacy-Preserving Biometric Authentication
- 2014
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 8788:2014, s. 293-294
-
Conference paper (peer-reviewed)
|
|
| 6. |
- Abidin, Aysajan, 1983, et al.
(author)
-
Security of a Privacy-Preserving Biometric Authentication Protocol Revisited
- 2014
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319122809 ; 8813, s. 290-304
-
Conference paper (peer-reviewed)abstract
- Biometric authentication establishes the identity of an individual based on biometric templates (e.g. fingerprints, retina scans etc.). Although biometric authentication has important advantages and many applications, it also raises serious security and privacy concerns. Here, we investigate a biometric authentication protocol that has been proposed by Bringer et al. and adopts a distributed architecture (i.e. multiple entities are involved in the authentication process). This protocol was proven to be secure and privacy-preserving in the honest-but-curious (or passive) attack model. We present an attack algorithm that can be employed to mount a number of attacks on the protocol under investigation. We then propose an improved version of the Bringer et al. protocol that is secure in the malicious (or active) insider attack model and has forward security.
|
|
| 7. |
- Aceto, L., et al.
(author)
-
Decompositional Reasoning about the History of Parallel Processes
- 2011
-
In: Fundamentals of software engineering. - Heidelberg : Springer Berlin/Heidelberg. - 1611-3349 .- 0302-9743. - 9783642293191 - 9783642293207 ; , s. 32-47
-
Conference paper (peer-reviewed)abstract
- This paper presents a decomposition technique for Hennessy-Milner logic with past and its extension with recursively defined formulae. In order to highlight the main ideas and technical tools, processes are described using a subset of CCS with parallel composition, nondeterministic choice, action prefixing and the inaction constant. The study focuses on developing decompositional reasoning techniques for parallel contexts in that language. © 2012 Springer-Verlag.
|
|
| 8. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
A Unified Approach for Static and Runtime Verification: Framework and Applications
- 2012
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642340253 ; :PART 1, s. 312-326
-
Conference paper (peer-reviewed)abstract
- Static verification of software is becoming ever more effective and efficient. Still, static techniques either have high precision, in which case powerful judgements are hard to achieve automatically, or they use abstractions supporting increased automation, but possibly losing important aspects of the concrete system in the process. Runtime verification has complementary strengths and weaknesses. It combines full precision of the model (including the real deployment environment) with full automation, but cannot judge future and alternative runs. Another drawback of runtime verification can be the computational overhead of monitoring the running system which, although typically not very high, can still be prohibitive in certain settings. In this paper, we propose a framework to combine static analysis techniques and runtime verification with the aim of getting the best of both techniques. In particular, we discuss an instantiation of our framework for the deductive theorem prover KeY, and the runtime verification tool LARVA. Apart from combining static and dynamic verification, this approach also combines the data centric analysis of KeY with the control centric analysis of LARVA. An advantage of the approach is that, through the use of a single specification which can be used by both analysis techniques, expensive parts of the analysis could be moved to the static phase, allowing the runtime monitor to make significant assumptions, dropping parts of expensive checks at runtime. We also discuss specific applications of our approach.
|
|
| 9. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
The KeY platform for verification and analysis of java programs
- 2014
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 8471:8471, s. 55-71
-
Conference paper (peer-reviewed)abstract
- The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flowsecurity, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.
|
|
| 10. |
- Albert, Elvira, et al.
(author)
-
Verified resource guarantees for heap manipulating programs
- 2012
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642288715 ; 7212, s. 130-145
-
Conference paper (peer-reviewed)abstract
- Program properties that are automatically inferred by static analysis tools are generally not considered to be completely trustworthy, unless the tool implementation or the results are formally verified. Here we focus on the formal verification of resource guarantees inferred by automatic cost analysis. Resource guarantees ensure that programs run within the indicated amount of resources which may refer to memory consumption, to number of instructions executed, etc. In previous work we studied formal verification of inferred resource guarantees that depend only on integer data. In realistic programs, however, resource consumption is often bounded by the size of heap-allocated data structures. Bounding their size requires to perform a number of structural heap analyses. The contributions of this paper are (i) to identify what exactly needs to be verified to guarantee sound analysis of heap manipulating programs, (ii) to provide a suitable extension of the program logic used for verification to handle structural heap properties in the context of resource guarantees, and (iii) to improve the underlying theorem prover so that proof obligations can be automatically discharged.
|
|
