-
Towards Stable Preferences for Stakeholder-aligned Machine Learning
Authors:
Haleema Sheraz,
Stefan C. Kremer,
Joshua August Skorburg,
Graham Taylor,
Walter Sinnott-Armstrong,
Kyle Boerstler
Abstract:
In response to the pressing challenge of kidney allocation, characterized by growing demands for organs, this research sets out to develop a data-driven solution to this problem, which also incorporates stakeholder values. The primary objective of this study is to create a method for learning both individual and group-level preferences pertaining to kidney allocations. Drawing upon data from the '…
▽ More
In response to the pressing challenge of kidney allocation, characterized by growing demands for organs, this research sets out to develop a data-driven solution to this problem, which also incorporates stakeholder values. The primary objective of this study is to create a method for learning both individual and group-level preferences pertaining to kidney allocations. Drawing upon data from the 'Pairwise Kidney Patient Online Survey.' Leveraging two distinct datasets and evaluating across three levels - Individual, Group and Stability - we employ machine learning classifiers assessed through several metrics. The Individual level model predicts individual participant preferences, the Group level model aggregates preferences across participants, and the Stability level model, an extension of the Group level, evaluates the stability of these preferences over time. By incorporating stakeholder preferences into the kidney allocation process, we aspire to advance the ethical dimensions of organ transplantation, contributing to more transparent and equitable practices while promoting the integration of moral values into algorithmic decision-making.
△ Less
Submitted 2 February, 2024; v1 submitted 26 January, 2024;
originally announced January 2024.
-
DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice
Authors:
Vincent Cheval,
Steve Kremer,
Itsaka Rakotonirina
Abstract:
Automated verification has become an essential part in the security evaluation of cryptographic protocols. In this context privacy-type properties are often modelled by indistinguishability statements, expressed as behavioural equivalences in a process calculus. In this paper we contribute both to the theory and practice of this verification problem. We establish new complexity results for static…
▽ More
Automated verification has become an essential part in the security evaluation of cryptographic protocols. In this context privacy-type properties are often modelled by indistinguishability statements, expressed as behavioural equivalences in a process calculus. In this paper we contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of protocol sessions. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives -- those that can be represented by a subterm convergent destructor rewrite system. We also implemented the procedure in a new tool, DeepSec. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raises the scope of the protocols that can be analysed.
△ Less
Submitted 11 March, 2024; v1 submitted 6 November, 2022;
originally announced November 2022.
-
The Exponentially Tilted Gaussian Prior for Variational Autoencoders
Authors:
Griffin Floto,
Stefan Kremer,
Mihai Nica
Abstract:
An important property for deep neural networks is the ability to perform robust out-of-distribution detection on previously unseen data. This property is essential for safety purposes when deploying models for real world applications. Recent studies show that probabilistic generative models can perform poorly on this task, which is surprising given that they seek to estimate the likelihood of trai…
▽ More
An important property for deep neural networks is the ability to perform robust out-of-distribution detection on previously unseen data. This property is essential for safety purposes when deploying models for real world applications. Recent studies show that probabilistic generative models can perform poorly on this task, which is surprising given that they seek to estimate the likelihood of training data. To alleviate this issue, we propose the exponentially tilted Gaussian prior distribution for the Variational Autoencoder (VAE) which pulls points onto the surface of a hyper-sphere in latent space. This achieves state-of-the art results on the area under the curve-receiver operator characteristics metric using just the log-likelihood that the VAE naturally assigns. Because this prior is a simple modification of the traditional VAE prior, it is faster and easier to implement than competitive methods.
△ Less
Submitted 12 April, 2022; v1 submitted 30 November, 2021;
originally announced November 2021.
-
Similarity Learning Networks for Animal Individual Re-Identification -- Beyond the Capabilities of a Human Observer
Authors:
Stefan Schneider,
Graham W. Taylor,
Stefan Linquist,
Stefan C. Kremer
Abstract:
Deep learning has become the standard methodology to approach computer vision tasks when large amounts of labeled data are available. One area where traditional deep learning approaches fail to perform is one-shot learning tasks where a model must correctly classify a new category after seeing only one example. One such domain is animal re-identification, an application of computer vision which ca…
▽ More
Deep learning has become the standard methodology to approach computer vision tasks when large amounts of labeled data are available. One area where traditional deep learning approaches fail to perform is one-shot learning tasks where a model must correctly classify a new category after seeing only one example. One such domain is animal re-identification, an application of computer vision which can be used globally as a method to automate species population estimates from camera trap images. Our work demonstrates both the application of similarity comparison networks to animal re-identification, as well as the capabilities of deep convolutional neural networks to generalize across domains. Few studies have considered animal re-identification methods across species. Here, we compare two similarity comparison methodologies: Siamese and Triplet-Loss, based on the AlexNet, VGG-19, DenseNet201, MobileNetV2, and InceptionV3 architectures considering mean average precision (mAP)@1 and mAP@5. We consider five data sets corresponding to five different species: humans, chimpanzees, humpback whales, fruit flies, and Siberian tigers, each with their own unique set of challenges. We demonstrate that Triplet Loss outperformed its Siamese counterpart for all species. Without any species-specific modifications, our results demonstrate that similarity comparison networks can reach a performance level beyond that of humans for the task of animal re-identification. The ability for researchers to re-identify an animal individual upon re-encounter is fundamental for addressing a broad range of questions in the study of population dynamics and community/behavioural ecology. Our expectation is that similarity comparison networks are the beginning of a major trend that could stand to revolutionize animal re-identification from camera trap data.
△ Less
Submitted 1 July, 2020; v1 submitted 21 February, 2019;
originally announced February 2019.
-
Past, Present, and Future Approaches Using Computer Vision for Animal Re-Identification from Camera Trap Data
Authors:
Stefan Schneider,
Graham W. Taylor,
Stefan S. Linquist,
Stefan C. Kremer
Abstract:
The ability of a researcher to re-identify (re-ID) an individual animal upon re-encounter is fundamental for addressing a broad range of questions in the study of ecosystem function, community and population dynamics, and behavioural ecology. In this review, we describe a brief history of camera traps for re-ID, present a collection of computer vision feature engineering methodologies previously u…
▽ More
The ability of a researcher to re-identify (re-ID) an individual animal upon re-encounter is fundamental for addressing a broad range of questions in the study of ecosystem function, community and population dynamics, and behavioural ecology. In this review, we describe a brief history of camera traps for re-ID, present a collection of computer vision feature engineering methodologies previously used for animal re-ID, provide an introduction to the underlying mechanisms of deep learning relevant to animal re-ID, highlight the success of deep learning methods for human re-ID, describe the few ecological studies currently utilizing deep learning for camera trap analyses, and our predictions for near future methodologies based on the rapid development of deep learning methods. By utilizing novel deep learning methods for object detection and similarity comparisons, ecologists can extract animals from an image/video data and train deep learning classifiers to re-ID animal individuals beyond the capabilities of a human observer. This methodology will allow ecologists with camera/video trap data to re-identify individuals that exit and re-enter the camera frame. Our expectation is that this is just the beginning of a major trend that could stand to revolutionize the analysis of camera trap data and, ultimately, our approach to animal ecology.
△ Less
Submitted 19 November, 2018;
originally announced November 2018.
-
Deep Learning Object Detection Methods for Ecological Camera Trap Data
Authors:
Stefan Schneider,
Graham W. Taylor,
Stefan C. Kremer
Abstract:
Deep learning methods for computer vision tasks show promise for automating the data analysis of camera trap images. Ecological camera traps are a common approach for monitoring an ecosystem's animal population, as they provide continual insight into an environment without being intrusive. However, the analysis of camera trap images is expensive, labour intensive, and time consuming. Recent advanc…
▽ More
Deep learning methods for computer vision tasks show promise for automating the data analysis of camera trap images. Ecological camera traps are a common approach for monitoring an ecosystem's animal population, as they provide continual insight into an environment without being intrusive. However, the analysis of camera trap images is expensive, labour intensive, and time consuming. Recent advances in the field of deep learning for object detection show promise towards automating the analysis of camera trap images. Here, we demonstrate their capabilities by training and comparing two deep learning object detection classifiers, Faster R-CNN and YOLO v2.0, to identify, quantify, and localize animal species within camera trap images using the Reconyx Camera Trap and the self-labeled Gold Standard Snapshot Serengeti data sets. When trained on large labeled datasets, object recognition methods have shown success. We demonstrate their use, in the context of realistically sized ecological data sets, by testing if object detection methods are applicable for ecological research scenarios when utilizing transfer learning. Faster R-CNN outperformed YOLO v2.0 with average accuracies of 93.0\% and 76.7\% on the two data sets, respectively. Our findings show promising steps towards the automation of the labourious task of labeling camera trap images, which can be used to improve our understanding of the population dynamics of ecosystems across the planet.
△ Less
Submitted 28 March, 2018;
originally announced March 2018.
-
Dynamic Tags for Security Protocols
Authors:
Myrto Arapinis,
Stéphanie Delaune,
Steve Kremer
Abstract:
The design and verification of cryptographic protocols is a notoriously difficult task, even in symbolic models which take an abstract view of cryptography. This is mainly due to the fact that protocols may interact with an arbitrary attacker which yields a verification problem that has several sources of unboundedness (size of messages, number of sessions, etc. In this paper, we characterize a cl…
▽ More
The design and verification of cryptographic protocols is a notoriously difficult task, even in symbolic models which take an abstract view of cryptography. This is mainly due to the fact that protocols may interact with an arbitrary attacker which yields a verification problem that has several sources of unboundedness (size of messages, number of sessions, etc. In this paper, we characterize a class of protocols for which deciding security for an unbounded number of sessions is decidable. More precisely, we present a simple transformation which maps a protocol that is secure for a bounded number of protocol sessions (a decidable problem) to a protocol that is secure for an unbounded number of sessions. The precise number of sessions that need to be considered is a function of the security property and we show that for several classical security properties a single session is sufficient. Therefore, in many cases our results yields a design strategy for security protocols: (i) design a protocol intended to be secure for a {single session}; and (ii) apply our transformation to obtain a protocol which is secure for an unbounded number of sessions.
△ Less
Submitted 17 June, 2014; v1 submitted 12 May, 2014;
originally announced May 2014.
-
Automated analysis of security protocols with global state
Authors:
Steve Kremer,
Robert Künnemann
Abstract:
Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, most existing automated verification tools do not support the analysis of such stateful security protocols - sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, whi…
▽ More
Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, most existing automated verification tools do not support the analysis of such stateful security protocols - sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, which are inherently monotonic. A notable exception is the recent tamarin prover which allows specifying protocols as multiset rewrite (msr) rules, a formalism expressive enough to encode state. As multiset rewriting is a "low-level" specification language with no direct support for concurrent message passing, encoding protocols correctly is a difficult and error-prone process. We propose a process calculus which is a variant of the applied pi calculus with constructs for manipulation of a global state by processes running in parallel. We show that this language can be translated to msr rules whilst preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a backend. We apply the tool to several case studies among which a simplified fragment of PKCS\#11, the Yubikey security token, and an optimistic contract signing protocol.
△ Less
Submitted 12 May, 2014; v1 submitted 5 March, 2014;
originally announced March 2014.
-
Focusing Testing by Using Inspection and Product Metrics
Authors:
Frank Elberzhager,
Stephan Kremer,
Jürgen Münch,
Danilo Assmann
Abstract:
A well-known approach for identifying defect-prone parts of software in order to focus testing is to use different kinds of product metrics such as size or complexity. Although this approach has been evaluated in many contexts, the question remains if there are further opportunities to improve test focusing. One idea is to identify other types of information that may indicate the location of defec…
▽ More
A well-known approach for identifying defect-prone parts of software in order to focus testing is to use different kinds of product metrics such as size or complexity. Although this approach has been evaluated in many contexts, the question remains if there are further opportunities to improve test focusing. One idea is to identify other types of information that may indicate the location of defect-prone software parts. Data from software inspections, in particular, appear to be promising. This kind of data might already lead to software parts that have inherent difficulties or programming challenges, and in consequence might be defect-prone. This article first explains how inspection and product metrics can be used to focus testing activities. Second, we compare selected product and inspection metrics commonly used to predict defect-prone parts (e.g., size and complexity metrics, inspection defect content metrics, and defect density metrics). Based on initial experience from two case studies performed in different environments, the suitability of different metrics for predicting defect-prone parts is illustrated. The studies revealed that inspection defect data seems to be a suitable predictor, and a combination of certain inspection and product metrics led to the best prioritizations in our contexts. In addition, qualitative experience is presented, which substantiates the expected benefit of using inspection results to optimize testing.
△ Less
Submitted 4 February, 2014; v1 submitted 30 January, 2014;
originally announced January 2014.
-
Guiding Testing Activities by Predicting Defect-prone Parts Using Product and Inspection Metrics
Authors:
Frank Elberzhager,
Stephan Kremer,
Jürgen Münch,
Danilo Assmann
Abstract:
Product metrics, such as size or complexity, are often used to identify defect-prone parts or to focus quality assurance activities. In contrast, quality information that is available early, such as information provided by inspections, is usually not used. Currently, only little experience is documented in the literature on whether data from early defect detection activities can support the identi…
▽ More
Product metrics, such as size or complexity, are often used to identify defect-prone parts or to focus quality assurance activities. In contrast, quality information that is available early, such as information provided by inspections, is usually not used. Currently, only little experience is documented in the literature on whether data from early defect detection activities can support the identification of defect-prone parts later in the development process. This article compares selected product and inspection metrics commonly used to predict defect-prone parts. Based on initial experience from two case studies performed in different environments, the suitability of different metrics for predicting defect-prone parts is illustrated. These studies revealed that inspection defect data seems to be a suitable predictor, and a combination of certain inspection and product metrics led to the best prioritizations in our contexts.
△ Less
Submitted 3 December, 2013;
originally announced December 2013.
-
Proceedings 7th International Workshop on Security Issues in Concurrency
Authors:
Michele Boreale,
Steve Kremer
Abstract:
This volume contains the proceedings of the 7th Workshop on Security Issues in Concurrency (SecCo'09). The workshop was held in Bologna, Italy on September 5th 2009, as a satellite workshop of CONCUR'09. The aim of the SecCo workshop series is to cover the gap between the security and the concurrency communities. More precisely, the workshop promotes the exchange of ideas, trying to focus on com…
▽ More
This volume contains the proceedings of the 7th Workshop on Security Issues in Concurrency (SecCo'09). The workshop was held in Bologna, Italy on September 5th 2009, as a satellite workshop of CONCUR'09. The aim of the SecCo workshop series is to cover the gap between the security and the concurrency communities. More precisely, the workshop promotes the exchange of ideas, trying to focus on common interests and stimulating discussions on central research questions. In particular, we called for papers dealing with security issues (such as authentication, integrity, privacy, confidentiality, access control, denial of service, service availability, safety aspects, fault tolerance, trust, language-based security, probabilistic and information theoretic models) in emerging fields like web services, mobile ad-hoc networks, agent-based infrastructures, peer-to-peer systems, context-aware computing, global/ubiquitous/pervasive computing.
△ Less
Submitted 22 October, 2009;
originally announced October 2009.
