| 1. |
- Hedin, Daniel, 1978, et al.
(author)
-
A Principled Approach to Tracking Information Flow in the Presence of Libraries
- 2017
-
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. - 9783662544549 ; 10204, s. 49-70
-
Conference paper (peer-reviewed)abstract
- There has been encouraging progress on information flow control for programs in increasingly complex programming languages, tracking the propagation of information from input sources to output sinks. Yet, programs are typically deployed in an environment with rich APIs and powerful libraries, posing challenges for information flow control when the code for these APIs and libraries is either unavailable or written in a different language.This paper presents a principled approach to tracking information flow in the presence of libraries. With the goal to strike the balance between security and precision, we present a framework that explores the middle ground between the “shallow”, signature-based modeling of libraries and the “deep”, stateful approach, where library models need to be supplied manually. We formalize our approach for a core language, extend it with lists and higher-order functions, and establish soundness results with respect to the security condition of noninterference.
|
|
| 2. |
- Abd Alrahman, Yehia, 1986, et al.
(author)
-
Testing for coordination fidelity : Testing for coordination fidelity
- 2019
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. ; , s. 152-169
-
Book chapter (peer-reviewed)abstract
- © Springer Nature Switzerland AG 2019. Operation control in modern distributed systems must rely on decentralised coordination among system participants. In particular when the operation control involves critical infrastructures such as power grids, it is vital to ensure correctness properties of such coordination mechanisms. In this paper, we present a verification technique that addresses coordination protocols for power grid operation control. Given a global protocol specification, we show how we can rely on testing semantics for the purpose of ensuring protocol fidelity, i.e., to certify that the interaction among the grid nodes follows the protocol specification.
|
|
| 3. |
- Abdelraheem, Mohamed, et al.
(author)
-
Practical Attacks on Relational Databases Protected via Searchable Encryption
- 2018
-
In: Lecture Notes in Computer Science. - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319991351 ; , s. 171-191
-
Conference paper (peer-reviewed)abstract
- Searchable symmetric encryption (SSE) schemes are commonly proposed to enable search in a protected unstructured documents such as email archives or any set of sensitive text files. However, some SSE schemes have been recently proposed in order to protect relational databases. Most of the previous attacks on SSE schemes have only targeted its common use case, protecting unstructured data. In this work, we propose a new inference attack on relational databases protected via SSE schemes. Our inference attack enables a passive adversary with only basic knowledge about the meta-data information of the target relational database to recover the attribute names of some observed queries. This violates query privacy since the attribute name of a query is secret.
|
|
| 4. |
- Abel, Andreas, 1974
(author)
-
Compositional coinduction with sized types
- 2016
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349.
-
Conference paper (peer-reviewed)
|
|
| 5. |
- Abidin, Aysajan, 1983, et al.
(author)
-
Efficient Verifiable Computation of XOR for Biometric Authentication
- 2016
-
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. ; 10052, s. 284-298
-
Conference paper (peer-reviewed)abstract
- This work addresses the security and privacy issues in remote biometric authentication by proposing an efficient mechanism to verify the correctness of the outsourced computation in such protocols. In particular, we propose an efficient verifiable computation of XORing encrypted messages using an XOR linear message authentication code (MAC) and we employ the proposed scheme to build a biometric authentication protocol. The proposed authentication protocol is both secure and privacy-preserving against malicious (as opposed to honest-but-curious) adversaries. Specifically, the use of the verifiable computation scheme together with an homomorphic encryption protects the privacy of biometric templates against malicious adversaries. Furthermore, in order to achieve unlinkability of authentication attempts, while keeping a low communication overhead, we show how to apply Oblivious RAM and biohashing to our protocol. We also provide a proof of security for the proposed solution. Our simulation results show that the proposed authentication protocol is efficient.
|
|
| 6. |
- Abrahamsson, Oskar, 1986, et al.
(author)
-
Automatically introducing tail recursion in CakeML
- 2018
-
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. ; 10788, s. 118-134
-
Conference paper (peer-reviewed)abstract
- We describe and implement an optimizing compiler transformation which turns non–tail-recursive functions into equivalent tail-recursive functions in an intermediate language of the CakeML compiler. CakeML is a strongly typed functional language based on Standard ML with call-by-value semantics and a fully verified compiler. We integrate our implementation into CakeML compiler, and provide a machine-checked proof verifying that the observational semantics of programs is preserved under the transformation. To the best of our knowledge, this is the first fully verified implementation of this transformation in any modern compiler. Moreover, our verification efforts uncover surprising drawbacks in some of the verification techniques employed in several parts of the CakeML compiler. We provide a work-around for these drawbacks, and compare it to potential alternatives.
|
|
| 7. |
- Adams, Robin, 1978, et al.
(author)
-
Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
- 2018
-
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. ; 11294, s. 196-214
-
Conference paper (peer-reviewed)abstract
- Privacy by design (PbD) is the principle that privacy should be considered at every stage of the software engineering process. It is increasingly both viewed as best practice and required by law. It is therefore desirable to have formal methods that provide guarantees that certain privacy-relevant properties hold. We propose an approach that can be used to design a privacy-compliant architecture without needing to know the source code or internal structure of any individual component. We model an architecture as a set of agents or components that pass messages to each other. We present in this paper algorithms that take as input an architecture and a set of privacy constraints, and output an extension of the original architecture that satisfies the privacy constraints.
|
|
| 8. |
- Adenskog, Magnus, 1985-, et al.
(author)
-
Balancing Potential and Risk : The Living Lab Approach in Mobile Participation Research
- 2017
-
In: Lecture Notes in Computer Science. - Cham : Springer Berlin/Heidelberg. - 0302-9743 .- 1611-3349. ; :10429, s. 12-23
-
Journal article (peer-reviewed)abstract
- Living labs as a research approach have been said to hold many promises regarding the evaluation of state-of-the art technologies in real-world contexts, for instance by allowing close cooperation with various stakeholders. At the same time, a living lab approach is connected with substantial complexity and increased risk. This paper elaborates on a conducted living lab with the objective to explore challenges and opportunities of mobile participation. For this purpose, a novel mobile application enabling interaction between citizens and city authorities was tested over a period of five months in Turku, Finland. In this paper, we describe identified risks associated with a living lab approach to mobile participation research. We conclude with an overall evaluation regarding the appropriateness of the living lab approach within the e-participation research field and provide recommendations on how to balance potential and risk in future projects.
|
|
| 9. |
- Afsharmazayejani, R., et al.
(author)
-
HoneyWiN : Novel honeycomb-based wireless NoC architecture in many-core era
- 2018
-
In: Lecture Notes in Computer Science. - Cham : Springer Verlag. - 0302-9743 .- 1611-3349. ; 10824 LNCS, s. 304-316
-
Journal article (peer-reviewed)abstract
- Although NoC-based systems with many cores are commercially available, their multi-hop nature has become a bottleneck on scaling performance and energy consumption parameters. Alternatively, hybrid wireless NoC provides a postern by exploiting single-hop express links for long-distance communications. Also, there is a common wisdom that grid-like mesh is the most stable topology in conventional designs. That is why almost all of the emerging architectures had been relying on this topology as well. In this paper, first we challenge the efficiency of the grid-like mesh in emerging systems. Then, we propose HoneyWiN, a hybrid reconfigurable wireless NoC architecture that relies on the honeycomb topology. The simulation results show that on average HoneyWiN saves 17% of energy consumption while increases the network throughput by 10% compared to its wireless mesh counterpart.
|
|
| 10. |
- Ahn, Ki Yung, et al.
(author)
-
Executable relational specifications of polymorphic type systems using prolog
- 2016
-
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. - 9783319296036 ; 9613, s. 109-125
-
Conference paper (peer-reviewed)abstract
- A concise, declarative, and machine executable specification of the Hindley–Milner type system (HM) can be formulated using logic programming languages such as Prolog. Modern functional language implementations such as the Glasgow Haskell Compiler support more extensive flavors of polymorphism beyond Milner’s theory of type polymorphism in the late 70's. We progressively extend the HM specification to include more advanced type system features. An interesting development is that extending dimensions of polymorphism beyond HM resulted in a multi-staged solution: resolve the typing relations first, while delaying to resolve kinding relations, and then resolve the delayed kinding relations. Our work demonstrates that logic programing is effective for prototyping polymorphic type systems with rich features of polymorphism, and that logic programming could have been even more effective for specifying type inference if it were equipped with better theories and tools for staged resolution of different relations at different levels.
|
|
