The management and specification of access control rules that enforce a given policy is a non-trivial, complex, and time consuming task. In this paper we aim at simplifying this task both at specification and verification levels. For that, we propose a formal model of Net filter, a firewall system integrated in the Linux kernel. We define an abstraction of the concepts of chains, rules, and packets existent in Net filter configurations, and give a semantics that mimics packet filtering and address translation. We then introduce a simple but powerful language that permits to specify firewall configurations that are unaffected by the relative ordering of rules, and that does not depend on the underlying Net filter chains. We give a semantics for this language and show that it can be translated into our Net filter abstraction. We then present Mignis, a publicly available tool that translates abstract firewall specifications into real Net filter configurations. Mignis is currently used to configure the whole firewall of the DAIS Department of Ca' Foscari University.

Oblivious transfer protocol is a basic building block in cryptography and is used to transfer information from a sender to a receiver in such a way that, at the end of the protocol, the sender does not know if the receiver got the message or not. Since Shor's quantum algorithm appeared, the security of most of the classical cryptographic schemes has been compromised, as they rely on the fact that factoring is infeasible. To overcome this, quantum mechanics has been used intensively in the past decades, and alternatives resistant to quantum attacks have been developed in order to fulfill the (potential) lack of security of a significant number of classical schemes. In this paper, we present a quantum computationally secure protocol for bit-string oblivious transfer between two parties, under the assumption of quantum hardness of state distinguishability and the constraint of performing at most few-qubit measurements (leaving open the question of general attacks performed on all qubits involved). The protocol is feasible, in the sense that it is implementable in polynomial time.

Partially supported by FCT grant SFRH/BD/8148/2002. Additional support from FEDER/FCT projects QuantLog POCI/MAT/55796/2004, QSec PTDC/EIA/67661/2006 and KLog PTDC/MAT/68723/2006. Partially supported by OSD/ONR CIP/SW URI “Software Quality and Infras