Showing 1–50 of 50 results for author: Chong, S

Gait-Adaptive Navigation and Human Searching in field with Cyborg Insect

Authors: Phuoc Thanh Tran-Ngoc, Huu Duoc Nguyen, Duc Long Le, Rui Li, Bing Sheng Chong, Hirotaka Sato

Abstract: This study focuses on improving the ability of cyborg insects to navigate autonomously during search and rescue missions in outdoor environments. We propose an algorithm that leverages data from an IMU to calculate orientation and position based on the insect's walking gait. These computed factors serve as essential feedback channels across 3 phases of our exploration. Our method functions without… ▽ More This study focuses on improving the ability of cyborg insects to navigate autonomously during search and rescue missions in outdoor environments. We propose an algorithm that leverages data from an IMU to calculate orientation and position based on the insect's walking gait. These computed factors serve as essential feedback channels across 3 phases of our exploration. Our method functions without relying on external systems. The results of our trials, carried out in both indoor (4.8 x 6.6 m^2) and outdoor (3.5 x 6.0 m^2) settings, show that the cyborg insect is capable of seeking a human without knowing the human's position. This exploration strategy would help to bring terrestrial cyborg insects closer to practical application in real-life search and rescue (SAR) missions. △ Less

Submitted 5 June, 2024; originally announced June 2024.

Comments: 35 pages, 9 figures

Preference Alignment with Flow Matching

Authors: Minu Kim, Yongsik Lee, Sehyeok Kang, Jihwan Oh, Song Chong, Seyoung Yun

Abstract: We present Preference Flow Matching (PFM), a new framework for preference-based reinforcement learning (PbRL) that streamlines the integration of preferences into an arbitrary class of pre-trained models. Existing PbRL methods require fine-tuning pre-trained models, which presents challenges such as scalability, inefficiency, and the need for model modifications, especially with black-box APIs lik… ▽ More We present Preference Flow Matching (PFM), a new framework for preference-based reinforcement learning (PbRL) that streamlines the integration of preferences into an arbitrary class of pre-trained models. Existing PbRL methods require fine-tuning pre-trained models, which presents challenges such as scalability, inefficiency, and the need for model modifications, especially with black-box APIs like GPT-4. In contrast, PFM utilizes flow matching techniques to directly learn from preference data, thereby reducing the dependency on extensive fine-tuning of pre-trained models. By leveraging flow-based models, PFM transforms less preferred data into preferred outcomes, and effectively aligns model outputs with human preferences without relying on explicit or implicit reward function estimation, thus avoiding common issues like overfitting in reward models. We provide theoretical insights that support our method's alignment with standard PbRL objectives. Experimental results indicate the practical effectiveness of our method, offering a new direction in aligning a pre-trained model to preference. △ Less

Submitted 30 May, 2024; originally announced May 2024.

PikeLPN: Mitigating Overlooked Inefficiencies of Low-Precision Neural Networks

Authors: Marina Neseem, Conor McCullough, Randy Hsin, Chas Leichner, Shan Li, In Suk Chong, Andrew G. Howard, Lukasz Lew, Sherief Reda, Ville-Mikko Rautio, Daniele Moro

Abstract: Low-precision quantization is recognized for its efficacy in neural network optimization. Our analysis reveals that non-quantized elementwise operations which are prevalent in layers such as parameterized activation functions, batch normalization, and quantization scaling dominate the inference cost of low-precision models. These non-quantized elementwise operations are commonly overlooked in SOTA… ▽ More Low-precision quantization is recognized for its efficacy in neural network optimization. Our analysis reveals that non-quantized elementwise operations which are prevalent in layers such as parameterized activation functions, batch normalization, and quantization scaling dominate the inference cost of low-precision models. These non-quantized elementwise operations are commonly overlooked in SOTA efficiency metrics such as Arithmetic Computation Effort (ACE). In this paper, we propose ACEv2 - an extended version of ACE which offers a better alignment with the inference cost of quantized models and their energy consumption on ML hardware. Moreover, we introduce PikeLPN, a model that addresses these efficiency issues by applying quantization to both elementwise operations and multiply-accumulate operations. In particular, we present a novel quantization technique for batch normalization layers named QuantNorm which allows for quantizing the batch normalization parameters without compromising the model performance. Additionally, we propose applying Double Quantization where the quantization scaling parameters are quantized. Furthermore, we recognize and resolve the issue of distribution mismatch in Separable Convolution layers by introducing Distribution-Heterogeneous Quantization which enables quantizing them to low-precision. PikeLPN achieves Pareto-optimality in efficiency-accuracy trade-off with up to 3X efficiency improvement compared to SOTA low-precision models. △ Less

Submitted 29 March, 2024; originally announced April 2024.

Comments: Accepted in CVPR 2024. 10 Figures, 9 Tables

Measuring Robustness in Cyber-Physical Systems under Sensor Attacks

Authors: Jian Xiang, Ruggero Lanotte, Simone Tini, Stephen Chong, Massimo Merro

Abstract: This paper contributes a formal framework for quantitative analysis of bounded sensor attacks on cyber-physical systems, using the formalism of differential dynamic logic. Given a precondition and postcondition of a system, we formalize two quantitative safety notions, quantitative forward and backward safety, which respectively express (1) how strong the strongest postcondition of the system is w… ▽ More This paper contributes a formal framework for quantitative analysis of bounded sensor attacks on cyber-physical systems, using the formalism of differential dynamic logic. Given a precondition and postcondition of a system, we formalize two quantitative safety notions, quantitative forward and backward safety, which respectively express (1) how strong the strongest postcondition of the system is with respect to the specified postcondition, and (2) how strong the specified precondition is with respect to the weakest precondition of the system needed to ensure the specified postcondition holds. We introduce two notions, forward and backward robustness, to characterize the robustness of a system against sensor attacks as the loss of safety. To reason about robustness, we introduce two simulation distances, forward and backward simulation distances, which are defined based on the behavioral distances between the original system and the system with compromised sensors. Forward and backward distances, respectively, characterize upper bounds of the degree of forward and backward safety loss caused by the sensor attacks. We verify the two simulation distances by expressing them as modalities, i.e., formulas of differential dynamic logic, and develop an ad-hoc proof system to reason with such formulas. We showcase our formal notions and reasoning techniques on two non-trivial case studies: an autonomous vehicle that needs to avoid collision and a water tank system. △ Less

Submitted 9 March, 2024; originally announced March 2024.

Comments: Preprint submitted to Elsevier

A prediction rigidity formalism for low-cost uncertainties in trained neural networks

Authors: Filippo Bigi, Sanggyu Chong, Michele Ceriotti, Federico Grasselli

Abstract: Regression methods are fundamental for scientific and technological applications. However, fitted models can be highly unreliable outside of their training domain, and hence the quantification of their uncertainty is crucial in many of their applications. Based on the solution of a constrained optimization problem, we propose "prediction rigidities" as a method to obtain uncertainties of arbitrary… ▽ More Regression methods are fundamental for scientific and technological applications. However, fitted models can be highly unreliable outside of their training domain, and hence the quantification of their uncertainty is crucial in many of their applications. Based on the solution of a constrained optimization problem, we propose "prediction rigidities" as a method to obtain uncertainties of arbitrary pre-trained regressors. We establish a strong connection between our framework and Bayesian inference, and we develop a last-layer approximation that allows the new method to be applied to neural networks. This extension affords cheap uncertainties without any modification to the neural network itself or its training procedure. We show the effectiveness of our method on a wide range of regression tasks, ranging from simple toy models to applications in chemistry and meteorology. △ Less

Submitted 4 March, 2024; originally announced March 2024.

Diffusion-based Neural Network Weights Generation

Authors: Bedionita Soro, Bruno Andreis, Hayeon Lee, Song Chong, Frank Hutter, Sung Ju Hwang

Abstract: Transfer learning is a topic of significant interest in recent deep learning research because it enables faster convergence and improved performance on new tasks. While the performance of transfer learning depends on the similarity of the source data to the target data, it is costly to train a model on a large number of datasets. Therefore, pretrained models are generally blindly selected with the… ▽ More Transfer learning is a topic of significant interest in recent deep learning research because it enables faster convergence and improved performance on new tasks. While the performance of transfer learning depends on the similarity of the source data to the target data, it is costly to train a model on a large number of datasets. Therefore, pretrained models are generally blindly selected with the hope that they will achieve good performance on the given task. To tackle such suboptimality of the pretrained models, we propose an efficient and adaptive transfer learning scheme through dataset-conditioned pretrained weights sampling. Specifically, we use a latent diffusion model with a variational autoencoder that can reconstruct the neural network weights, to learn the distribution of a set of pretrained weights conditioned on each dataset for transfer learning on unseen datasets. By learning the distribution of a neural network on a variety pretrained models, our approach enables adaptive sampling weights for unseen datasets achieving faster convergence and reaching competitive performance. △ Less

Submitted 28 February, 2024; originally announced February 2024.

Comments: 14 pages

Graph-Network-Based Predictive Modeling for Highly Cross-Linked Polymer Systems

Authors: Wonseok Lee, Sanggyu Chong, Jihan Kim

Abstract: In this study, a versatile methodology for initiating polymerization from monomers in highly cross-linked materials is investigated. As polymerization progresses, force-field parameters undergo continuous modification due to the formation of new chemical bonds. This dynamic process not only impacts the atoms directly involved in bonding, but also influences the neighboring atomic environment. Moni… ▽ More In this study, a versatile methodology for initiating polymerization from monomers in highly cross-linked materials is investigated. As polymerization progresses, force-field parameters undergo continuous modification due to the formation of new chemical bonds. This dynamic process not only impacts the atoms directly involved in bonding, but also influences the neighboring atomic environment. Monitoring these complex changes in highly cross-linked structures poses a challenge. To address this issue, we introduce a graph-network-based algorithm that offers both rapid and accurate predictions. The algorithm merges polymer construction protocols with LAMMPS, a large-scale molecular dynamics simulation software. The adaptability of this code has been demonstrated by its successful application to various amorphous polymers, including porous polymer networks (PPNs), and epoxy-resins, while the algorithm has been employed for additional tasks, such as implementing pore-piercing deformations and calculating material properties. △ Less

Submitted 21 December, 2023; originally announced January 2024.

Fast Estimations of Hitting Time of Elitist Evolutionary Algorithms from Fitness Levels

Authors: Jun He, Siang Yew Chong, Xin Yao

Abstract: The fitness level method is an easy-to-use tool for estimating the hitting time of elitist evolutionary algorithms. Recently, linear lower and upper bounds by fitness levels have been constructed. But these bounds require recursive computation, which makes them difficult to use in practice. We address this shortcoming with a new directed graph (digraph) method that does not require recursive compu… ▽ More The fitness level method is an easy-to-use tool for estimating the hitting time of elitist evolutionary algorithms. Recently, linear lower and upper bounds by fitness levels have been constructed. But these bounds require recursive computation, which makes them difficult to use in practice. We address this shortcoming with a new directed graph (digraph) method that does not require recursive computation and significantly simplifies the calculation of coefficients in the lower bound. In the method, we select a sub-digraph and divide it into fitness levels, then construct an explicit formula for computing the linear lower bound coefficients using transition probabilities restricted to the subdigraph. A major advantage of the new method is the derivation of tight lower bounds on fitness functions with shortcuts, which are difficult to achieve using previous fitness methods. We use three examples (FullyDeceptive, TwoMax1 and Deceptive) to demonstrate that each new lower bound is tight, but previous lower bounds are not. Our work significantly extends the fitness level method from addressing simple fitness functions without shortcuts to more complex functions with shortcuts. △ Less

Submitted 16 May, 2024; v1 submitted 17 November, 2023; originally announced November 2023.

Guess & Sketch: Language Model Guided Transpilation

Authors: Celine Lee, Abdulrahman Mahmoud, Michal Kurek, Simone Campanoni, David Brooks, Stephen Chong, Gu-Yeon Wei, Alexander M. Rush

Abstract: Maintaining legacy software requires many software and systems engineering hours. Assembly code programs, which demand low-level control over the computer machine state and have no variable names, are particularly difficult for humans to analyze. Existing conventional program translators guarantee correctness, but are hand-engineered for the source and target programming languages in question. Lea… ▽ More Maintaining legacy software requires many software and systems engineering hours. Assembly code programs, which demand low-level control over the computer machine state and have no variable names, are particularly difficult for humans to analyze. Existing conventional program translators guarantee correctness, but are hand-engineered for the source and target programming languages in question. Learned transpilation, i.e. automatic translation of code, offers an alternative to manual re-writing and engineering efforts. Automated symbolic program translation approaches guarantee correctness but struggle to scale to longer programs due to the exponentially large search space. Their rigid rule-based systems also limit their expressivity, so they can only reason about a reduced space of programs. Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness. In this work, we leverage the strengths of LMs and symbolic solvers in a neurosymbolic approach to learned transpilation for assembly code. Assembly code is an appropriate setting for a neurosymbolic approach, since assembly code can be divided into shorter non-branching basic blocks amenable to the use of symbolic methods. Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence of the transpilation input and output. We test Guess & Sketch on three different test sets of assembly transpilation tasks, varying in difficulty, and show that it successfully transpiles 57.6% more examples than GPT-4 and 39.6% more examples than an engineered transpiler. We also share a training and evaluation dataset for this task. △ Less

Submitted 15 March, 2024; v1 submitted 25 September, 2023; originally announced September 2023.

Modular, Multi-Robot Integration of Laboratories: An Autonomous Solid-State Workflow for Powder X-Ray Diffraction

Authors: Amy. M. Lunt, Hatem Fakhruldeen, Gabriella Pizzuto, Louis Longley, Alexander White, Nicola Rankin, Rob Clowes, Ben Alston, Lucia Gigli, Graeme M. Day, Andrew I. Cooper, Sam. Y. Chong

Abstract: Automation can transform productivity in research activities that use liquid handling, such as organic synthesis, but it has made less impact in materials laboratories, which require sample preparation steps and a range of solid-state characterization techniques. For example, powder X-ray diffraction (PXRD) is a key method in materials and pharmaceutical chemistry, but its end-to-end automation is… ▽ More Automation can transform productivity in research activities that use liquid handling, such as organic synthesis, but it has made less impact in materials laboratories, which require sample preparation steps and a range of solid-state characterization techniques. For example, powder X-ray diffraction (PXRD) is a key method in materials and pharmaceutical chemistry, but its end-to-end automation is challenging because it involves solid powder handling and sample processing. Here we present a fully autonomous solid-state workflow for PXRD experiments that can match or even surpass manual data quality. The workflow involves 12 steps performed by a team of three multipurpose robots, illustrating the power of flexible, modular automation to integrate complex, multitask laboratories. △ Less

Submitted 23 November, 2023; v1 submitted 1 September, 2023; originally announced September 2023.

Beyond the Snapshot: Brain Tokenized Graph Transformer for Longitudinal Brain Functional Connectome Embedding

Authors: Zijian Dong, Yilei Wu, Yu Xiao, Joanna Su Xian Chong, Yueming Jin, Juan Helen Zhou

Abstract: Under the framework of network-based neurodegeneration, brain functional connectome (FC)-based Graph Neural Networks (GNN) have emerged as a valuable tool for the diagnosis and prognosis of neurodegenerative diseases such as Alzheimer's disease (AD). However, these models are tailored for brain FC at a single time point instead of characterizing FC trajectory. Discerning how FC evolves with diseas… ▽ More Under the framework of network-based neurodegeneration, brain functional connectome (FC)-based Graph Neural Networks (GNN) have emerged as a valuable tool for the diagnosis and prognosis of neurodegenerative diseases such as Alzheimer's disease (AD). However, these models are tailored for brain FC at a single time point instead of characterizing FC trajectory. Discerning how FC evolves with disease progression, particularly at the predementia stages such as cognitively normal individuals with amyloid deposition or individuals with mild cognitive impairment (MCI), is crucial for delineating disease spreading patterns and developing effective strategies to slow down or even halt disease advancement. In this work, we proposed the first interpretable framework for brain FC trajectory embedding with application to neurodegenerative disease diagnosis and prognosis, namely Brain Tokenized Graph Transformer (Brain TokenGT). It consists of two modules: 1) Graph Invariant and Variant Embedding (GIVE) for generation of node and spatio-temporal edge embeddings, which were tokenized for downstream processing; 2) Brain Informed Graph Transformer Readout (BIGTR) which augments previous tokens with trainable type identifiers and non-trainable node identifiers and feeds them into a standard transformer encoder to readout. We conducted extensive experiments on two public longitudinal fMRI datasets of the AD continuum for three tasks, including differentiating MCI from controls, predicting dementia conversion in MCI, and classification of amyloid positive or negative cognitively normal individuals. Based on brain FC trajectory, the proposed Brain TokenGT approach outperformed all the other benchmark models and at the same time provided excellent interpretability. The code is available at https://github.com/ZijianD/Brain-TokenGT.git △ Less

Submitted 12 July, 2023; v1 submitted 3 July, 2023; originally announced July 2023.

Comments: MICCAI 2023

From Plate to Prevention: A Dietary Nutrient-aided Platform for Health Promotion in Singapore

Authors: Kaiping Zheng, Thao Nguyen, Jesslyn Hwei Sing Chong, Charlene Enhui Goh, Melanie Herschel, Hee Hoon Lee, Changshuo Liu, Beng Chin Ooi, Wei Wang, James Yip

Abstract: Singapore has been striving to improve the provision of healthcare services to her people. In this course, the government has taken note of the deficiency in regulating and supervising people's nutrient intake, which is identified as a contributing factor to the development of chronic diseases. Consequently, this issue has garnered significant attention. In this paper, we share our experience in a… ▽ More Singapore has been striving to improve the provision of healthcare services to her people. In this course, the government has taken note of the deficiency in regulating and supervising people's nutrient intake, which is identified as a contributing factor to the development of chronic diseases. Consequently, this issue has garnered significant attention. In this paper, we share our experience in addressing this issue and attaining medical-grade nutrient intake information to benefit Singaporeans in different aspects. To this end, we develop the FoodSG platform to incubate diverse healthcare-oriented applications as a service in Singapore, taking into account their shared requirements. We further identify the profound meaning of localized food datasets and systematically clean and curate a localized Singaporean food dataset FoodSG-233. To overcome the hurdle in recognition performance brought by Singaporean multifarious food dishes, we propose to integrate supervised contrastive learning into our food recognition model FoodSG-SCL for the intrinsic capability to mine hard positive/negative samples and therefore boost the accuracy. Through a comprehensive evaluation, we present performance results of the proposed model and insights on food-related healthcare applications. The FoodSG-233 dataset has been released in https://foodlg.comp.nus.edu.sg/. △ Less

Submitted 28 March, 2023; v1 submitted 10 January, 2023; originally announced January 2023.

Resilient Set-based State Estimation for Linear Time-Invariant Systems Using Zonotopes

Authors: Muhammad Umar B. Niazi, Amr Alanwar, Michelle S. Chong, Karl Henrik Johansson

Abstract: This paper considers the problem of set-based state estimation for linear time-invariant (LTI) systems under time-varying sensor attacks. Provided that the LTI system is stable and observable via every single sensor and that at least one sensor is uncompromised, we guarantee that the true state is always contained in the estimated set. We use zonotopes to represent these sets for computational eff… ▽ More This paper considers the problem of set-based state estimation for linear time-invariant (LTI) systems under time-varying sensor attacks. Provided that the LTI system is stable and observable via every single sensor and that at least one sensor is uncompromised, we guarantee that the true state is always contained in the estimated set. We use zonotopes to represent these sets for computational efficiency. However, we show that intelligently designed stealthy attacks may cause exponential growth in the algorithm's worst-case complexity. We present several strategies to handle this complexity issue and illustrate our resilient zonotope-based state estimation algorithm on a rotating target system. △ Less

Submitted 15 November, 2022; originally announced November 2022.

CTooth+: A Large-scale Dental Cone Beam Computed Tomography Dataset and Benchmark for Tooth Volume Segmentation

Authors: Weiwei Cui, Yaqi Wang, Yilong Li, Dan Song, Xingyong Zuo, Jiaojiao Wang, Yifan Zhang, Huiyu Zhou, Bung san Chong, Liaoyuan Zeng, Qianni Zhang

Abstract: Accurate tooth volume segmentation is a prerequisite for computer-aided dental analysis. Deep learning-based tooth segmentation methods have achieved satisfying performances but require a large quantity of tooth data with ground truth. The dental data publicly available is limited meaning the existing methods can not be reproduced, evaluated and applied in clinical practice. In this paper, we esta… ▽ More Accurate tooth volume segmentation is a prerequisite for computer-aided dental analysis. Deep learning-based tooth segmentation methods have achieved satisfying performances but require a large quantity of tooth data with ground truth. The dental data publicly available is limited meaning the existing methods can not be reproduced, evaluated and applied in clinical practice. In this paper, we establish a 3D dental CBCT dataset CTooth+, with 22 fully annotated volumes and 146 unlabeled volumes. We further evaluate several state-of-the-art tooth volume segmentation strategies based on fully-supervised learning, semi-supervised learning and active learning, and define the performance principles. This work provides a new benchmark for the tooth volume segmentation task, and the experiment can serve as the baseline for future AI-based dental imaging research and clinical application development. △ Less

Submitted 2 August, 2022; originally announced August 2022.

The StarCraft Multi-Agent Challenges+ : Learning of Multi-Stage Tasks and Environmental Factors without Precise Reward Functions

Authors: Mingyu Kim, Jihwan Oh, Yongsik Lee, Joonkee Kim, Seonghwan Kim, Song Chong, Se-Young Yun

Abstract: In this paper, we propose a novel benchmark called the StarCraft Multi-Agent Challenges+, where agents learn to perform multi-stage tasks and to use environmental factors without precise reward functions. The previous challenges (SMAC) recognized as a standard benchmark of Multi-Agent Reinforcement Learning are mainly concerned with ensuring that all agents cooperatively eliminate approaching adve… ▽ More In this paper, we propose a novel benchmark called the StarCraft Multi-Agent Challenges+, where agents learn to perform multi-stage tasks and to use environmental factors without precise reward functions. The previous challenges (SMAC) recognized as a standard benchmark of Multi-Agent Reinforcement Learning are mainly concerned with ensuring that all agents cooperatively eliminate approaching adversaries only through fine manipulation with obvious reward functions. This challenge, on the other hand, is interested in the exploration capability of MARL algorithms to efficiently learn implicit multi-stage tasks and environmental factors as well as micro-control. This study covers both offensive and defensive scenarios. In the offensive scenarios, agents must learn to first find opponents and then eliminate them. The defensive scenarios require agents to use topographic features. For example, agents need to position themselves behind protective structures to make it harder for enemies to attack. We investigate MARL algorithms under SMAC+ and observe that recent approaches work well in similar settings to the previous challenges, but misbehave in offensive scenarios. Additionally, we observe that an enhanced exploration approach has a positive effect on performance but is not able to completely solve all scenarios. This study proposes new directions for future research. △ Less

Submitted 7 July, 2022; v1 submitted 5 July, 2022; originally announced July 2022.

Comments: ICML Workshop: AI for Agent Based Modeling 2022 Spotlight

Approximating Permutations with Neural Network Components for Travelling Photographer Problem

Authors: Sue Sin Chong

Abstract: Most of the current inference techniques rely upon Bayesian inference on Probabilistic Graphical Models of observations and do predictions and classification on observations. However, there is very little literature on the mining of relationships between observations and building models of the relationship between sets of observations or the generating context of the observations. Moreover, event… ▽ More Most of the current inference techniques rely upon Bayesian inference on Probabilistic Graphical Models of observations and do predictions and classification on observations. However, there is very little literature on the mining of relationships between observations and building models of the relationship between sets of observations or the generating context of the observations. Moreover, event understanding of machines with observation inputs needs to understand the relationship between observations. Thus there is a crucial need to build models and develop effective data structures to accumulate and organize relationships between observations. Given a PGM model, this paper attempts to fit a permutation of states to a sequence of observation tokens (The Travelling Photographer Problem). We have devised a machine learning inspired architecture for randomized approximation of state permutation, facilitating parallelization of heuristic search of permutations. As a result, our algorithm can solve The Travelling Photographer Problem with minimal error. Furthermore, we demonstrate that by mimicking machine learning components such as normalization, dropout, and lambda layer with a randomized algorithm, we can devise an architecture that solves TPP, a permutation NP-Hard problem. Other than TPP, we can also provide a 2-Local improvement heuristic for the Travelling Salesman Problem (TSP) with similar ideas. △ Less

Submitted 23 May, 2022; v1 submitted 30 April, 2022; originally announced May 2022.

Comments: 11 pages

Journal ref: Published in 2022 Asia Conference on Algorithms, Computing and Machine Learning (CACML 2022)

Loss Function Entropy Regularization for Diverse Decision Boundaries

Authors: Sue Sin Chong

Abstract: Is it possible to train several classifiers to perform meaningful crowd-sourcing to produce a better prediction label set without ground-truth annotation? This paper will modify the contrastive learning objectives to automatically train a self-complementing ensemble to produce a state-of-the-art prediction on the CIFAR10 and CIFAR100-20 tasks. This paper will present a straightforward method to mo… ▽ More Is it possible to train several classifiers to perform meaningful crowd-sourcing to produce a better prediction label set without ground-truth annotation? This paper will modify the contrastive learning objectives to automatically train a self-complementing ensemble to produce a state-of-the-art prediction on the CIFAR10 and CIFAR100-20 tasks. This paper will present a straightforward method to modify a single unsupervised classification pipeline to automatically generate an ensemble of neural networks with varied decision boundaries to learn a more extensive feature set of classes. Loss Function Entropy Regularization (LFER) are regularization terms to be added to the pre-training and contrastive learning loss functions. LFER is a gear to modify the entropy state of the output space of unsupervised learning, thereby diversifying the latent representation of decision boundaries of neural networks. Ensemble trained with LFER has higher successful prediction accuracy for samples near decision boundaries. LFER is an adequate gear to perturb decision boundaries and has produced classifiers that beat state-of-the-art at the contrastive learning stage. Experiments show that LFER can produce an ensemble with accuracy comparable to the state-of-the-art yet have varied latent decision boundaries. It allows us to perform meaningful verification for samples near decision boundaries, encouraging the correct classification of near-boundary samples. By compounding the probability of correct prediction of a single sample amongst an ensemble of neural network trained, our method can improve upon a single classifier by denoising and affirming correct feature mappings. △ Less

Submitted 23 May, 2022; v1 submitted 30 April, 2022; originally announced May 2022.

Comments: 7 pages

Journal ref: 2022 7th International Conference on Big Data Analytics (ICBDA)

Towards Porting Operating Systems with Program Synthesis

Authors: Jingmei Hu, Eric Lu, David A. Holland, Ming Kawaguchi, Stephen Chong, Margo I. Seltzer

Abstract: The end of Moore's Law has ushered in a diversity of hardware not seen in decades. Operating system (and system software) portability is accordingly becoming increasingly critical. Simultaneously, there has been tremendous progress in program synthesis. We set out to explore the feasibility of using modern program synthesis to generate the machine-dependent parts of an operating system. Our ultima… ▽ More The end of Moore's Law has ushered in a diversity of hardware not seen in decades. Operating system (and system software) portability is accordingly becoming increasingly critical. Simultaneously, there has been tremendous progress in program synthesis. We set out to explore the feasibility of using modern program synthesis to generate the machine-dependent parts of an operating system. Our ultimate goal is to generate new ports automatically from descriptions of new machines. One of the issues involved is writing specifications, both for machine-dependent operating system functionality and for instruction set architectures. We designed two domain-specific languages: Alewife for machine-independent specifications of machine-dependent operating system functionality and Cassiopea for describing instruction set architecture semantics. Automated porting also requires an implementation. We developed a toolchain that, given an Alewife specification and a Cassiopea machine description, specializes the machine-independent specification to the target instruction set architecture and synthesizes an implementation in assembly language with a customized symbolic execution engine. Using this approach, we demonstrate successful synthesis of a total of 140 OS components from two pre-existing OSes for four real hardware platforms. We also developed several optimization methods for OS-related assembly synthesis to improve scalability. The effectiveness of our languages and ability to synthesize code for all 140 specifications is evidence of the feasibility of program synthesis for machine-dependent OS code. However, many research challenges remain; we also discuss the benefits and limitations of our synthesis-based approach to automated OS porting. △ Less

Submitted 22 September, 2022; v1 submitted 15 April, 2022; originally announced April 2022.

Comments: ACM Transactions on Programming Languages and Systems. Accepted on August 2022

HELP: Hardware-Adaptive Efficient Latency Prediction for NAS via Meta-Learning

Authors: Hayeon Lee, Sewoong Lee, Song Chong, Sung Ju Hwang

Abstract: For deployment, neural architecture search should be hardware-aware, in order to satisfy the device-specific constraints (e.g., memory usage, latency and energy consumption) and enhance the model efficiency. Existing methods on hardware-aware NAS collect a large number of samples (e.g., accuracy and latency) from a target device, either builds a lookup table or a latency estimator. However, such a… ▽ More For deployment, neural architecture search should be hardware-aware, in order to satisfy the device-specific constraints (e.g., memory usage, latency and energy consumption) and enhance the model efficiency. Existing methods on hardware-aware NAS collect a large number of samples (e.g., accuracy and latency) from a target device, either builds a lookup table or a latency estimator. However, such approach is impractical in real-world scenarios as there exist numerous devices with different hardware specifications, and collecting samples from such a large number of devices will require prohibitive computational and monetary cost. To overcome such limitations, we propose Hardware-adaptive Efficient Latency Predictor (HELP), which formulates the device-specific latency estimation problem as a meta-learning problem, such that we can estimate the latency of a model's performance for a given task on an unseen device with a few samples. To this end, we introduce novel hardware embeddings to embed any devices considering them as black-box functions that output latencies, and meta-learn the hardware-adaptive latency predictor in a device-dependent manner, using the hardware embeddings. We validate the proposed HELP for its latency estimation performance on unseen platforms, on which it achieves high estimation performance with as few as 10 measurement samples, outperforming all relevant baselines. We also validate end-to-end NAS frameworks using HELP against ones without it, and show that it largely reduces the total time cost of the base NAS method, in latency-constrained settings. Code is available at https://github.com/HayeonLee/HELP. △ Less

Submitted 1 December, 2021; v1 submitted 16 June, 2021; originally announced June 2021.

Comments: NeurIPS 2021 (Spotlight)

Relational Analysis of Sensor Attacks on Cyber-Physical Systems

Authors: Jian Xiang, Nathan Fulton, Stephen Chong

Abstract: Cyber-physical systems, such as self-driving cars or autonomous aircraft, must defend against attacks that target sensor hardware. Analyzing system design can help engineers understand how a compromised sensor could impact the system's behavior; however, designing security analyses for cyber-physical systems is difficult due to their combination of discrete dynamics, continuous dynamics, and nonde… ▽ More Cyber-physical systems, such as self-driving cars or autonomous aircraft, must defend against attacks that target sensor hardware. Analyzing system design can help engineers understand how a compromised sensor could impact the system's behavior; however, designing security analyses for cyber-physical systems is difficult due to their combination of discrete dynamics, continuous dynamics, and nondeterminism. This paper contributes a framework for modeling and analyzing sensor attacks on cyber-physical systems, using the formalism of hybrid programs. We formalize and analyze two relational properties of a system's robustness. These relational properties respectively express (1) whether a system's safety property can be influenced by sensor attacks, and (2) whether a system's high-integrity state can be affected by sensor attacks. We characterize these relational properties by defining an equivalence relation between a system under attack and the original unattacked system. That is, the system satisfies the robustness properties if executions of the attacked system are appropriately related to executions of the unattacked system. We present two techniques for reasoning about the equivalence relation and thus proving the relational properties for a system. One proof technique decomposes large proof obligations to smaller proof obligations. The other proof technique adapts the self-composition technique from the literature on secure information-flow, allowing us to reduce reasoning about the equivalence of two systems to reasoning about properties of a single system. This technique allows us to reuse existing tools for reasoning about properties of hybrid programs, but is challenging due to the combination of discrete dynamics, continuous dynamics, and nondeterminism. To evaluate, we present three case studies motivated by real design flaws in existing cyber-physical systems. △ Less

Submitted 3 June, 2021; originally announced June 2021.

Comments: This is an extended version of the paper with the same title that appeared in the 2021 Computer Security Foundations Symposium

Insect-Computer Hybrid System for Autonomous Search and Rescue Mission

Authors: P. Thanh Tran-Ngoc, D. Long Le, Bing Sheng Chong, H. Duoc Nguyen, V. Than Dung, Feng Cao, Yao Li, Kazuki Kai, Jia Hui Gan, T. Thang Vo-Doan, T. Luan Nguyen, Hirotaka Sato

Abstract: There is still a long way to go before artificial mini robots are really used for search and rescue missions in disaster-hit areas due to hindrance in power consumption, computation load of the locomotion, and obstacle-avoidance system. Insect-computer hybrid system, which is the fusion of living insect platform and microcontroller, emerges as an alternative solution. This study demonstrates the f… ▽ More There is still a long way to go before artificial mini robots are really used for search and rescue missions in disaster-hit areas due to hindrance in power consumption, computation load of the locomotion, and obstacle-avoidance system. Insect-computer hybrid system, which is the fusion of living insect platform and microcontroller, emerges as an alternative solution. This study demonstrates the first-ever insect-computer hybrid system conceived for search and rescue missions, which is capable of autonomous navigation and human presence detection in an unstructured environment. Customized navigation control algorithm utilizing the insect's intrinsic navigation capability achieved exploration and negotiation of complex terrains. On-board high-accuracy human presence detection using infrared camera was achieved with a custom machine learning model. Low power consumption suggests system suitability for hour-long operations and its potential for realization in real-life missions. △ Less

Submitted 21 June, 2021; v1 submitted 23 May, 2021; originally announced May 2021.

Comments: Videos are available at https://hirosatontu.wordpress.com/research/

A Calculus for Flow-Limited Authorization

Authors: Owen Arden, Anitha Gollamudi, Ethan Cecchetti, Stephen Chong, Andrew C. Myers

Abstract: Real-world applications routinely make authorization decisions based on dynamic computation. Reasoning about dynamically computed authority is challenging. Integrity of the system might be compromised if attackers can improperly influence the authorizing computation. Confidentiality can also be compromised by authorization, since authorization decisions are often based on sensitive data such as me… ▽ More Real-world applications routinely make authorization decisions based on dynamic computation. Reasoning about dynamically computed authority is challenging. Integrity of the system might be compromised if attackers can improperly influence the authorizing computation. Confidentiality can also be compromised by authorization, since authorization decisions are often based on sensitive data such as membership lists and passwords. Previous formal models for authorization do not fully address the security implications of permitting trust relationships to change, which limits their ability to reason about authority that derives from dynamic computation. Our goal is an approach to constructing dynamic authorization mechanisms that do not violate confidentiality or integrity. The Flow-Limited Authorization Calculus (FLAC) is a simple, expressive model for reasoning about dynamic authorization as well as an information flow control language for securely implementing various authorization mechanisms. FLAC combines the insights of two previous models: it extends the Dependency Core Calculus with features made possible by the Flow-Limited Authorization Model. FLAC provides strong end-to-end information security guarantees even for programs that incorporate and implement rich dynamic authorization mechanisms. These guarantees include noninterference and robust declassification, which prevent attackers from influencing information disclosures in unauthorized ways. We prove these security properties formally for all FLAC programs and explore the expressiveness of FLAC with several examples. △ Less

Submitted 21 April, 2021; originally announced April 2021.

Comments: 58 pages

ACM Class: F.3.1; F.3.2; D.4.6

Towards Complex and Continuous Manipulation: A Gesture Based Anthropomorphic Robotic Hand Design

Authors: Li Tian, Hanhui Li, Qifa Wang, Xuezeng Du, Jialin Tao, Jordan Sia Chong, Nadia Magnenat Thalmann, Jianmin Zheng

Abstract: Most current anthropomorphic robotic hands can realize part of the human hand functions, particularly for object grasping. However, due to the complexity of the human hand, few current designs target at daily object manipulations, even for simple actions like rotating a pen. To tackle this problem, we introduce a gesture based framework, which adopts the widely-used 33 grasping gestures of Feix as… ▽ More Most current anthropomorphic robotic hands can realize part of the human hand functions, particularly for object grasping. However, due to the complexity of the human hand, few current designs target at daily object manipulations, even for simple actions like rotating a pen. To tackle this problem, we introduce a gesture based framework, which adopts the widely-used 33 grasping gestures of Feix as the bases for hand design and implementation of manipulation. In the proposed framework, we first measure the motion ranges of human fingers for each gesture, and based on the results, we propose a simple yet dexterous robotic hand design with 13 degrees of actuation. Furthermore, we adopt a frame interpolation based method, in which we consider the base gestures as the key frames to represent a manipulation task, and use the simple linear interpolation strategy to accomplish the manipulation. To demonstrate the effectiveness of our framework, we define a three-level benchmark, which includes not only 62 test gestures from previous research, but also multiple complex and continuous actions. Experimental results on this benchmark validate the dexterity of the proposed design and our video is available in \url{https://drive.google.com/file/d/1wPtkd2P0zolYSBW7_3tVMUHrZEeXLXgD/view?usp=sharing}. △ Less

Submitted 20 April, 2021; v1 submitted 20 December, 2020; originally announced December 2020.

Comments: 8 pages, 9 figures, 3 tables, accepted by IEEE Robotics and Automation Letters

Formulog: Datalog for SMT-Based Static Analysis (Extended Version)

Authors: Aaron Bembenek, Michael Greenberg, Stephen Chong

Abstract: Satisfiability modulo theories (SMT) solving has become a critical part of many static analyses, including symbolic execution, refinement type checking, and model checking. We propose Formulog, a domain-specific language that makes it possible to write a range of SMT-based static analyses in a way that is both close to their formal specifications and amenable to high-level optimizations and effici… ▽ More Satisfiability modulo theories (SMT) solving has become a critical part of many static analyses, including symbolic execution, refinement type checking, and model checking. We propose Formulog, a domain-specific language that makes it possible to write a range of SMT-based static analyses in a way that is both close to their formal specifications and amenable to high-level optimizations and efficient evaluation. Formulog extends the logic programming language Datalog with a first-order functional language and mechanisms for representing and reasoning about SMT formulas; a novel type system supports the construction of expressive formulas, while ensuring that neither normal evaluation nor SMT solving goes wrong. Our case studies demonstrate that a range of SMT-based analyses can naturally and concisely be encoded in Formulog, and that -- thanks to this encoding -- high-level Datalog-style optimizations can be automatically and advantageously applied to these analyses. △ Less

Submitted 16 October, 2020; v1 submitted 17 September, 2020; originally announced September 2020.

Comments: Please cite the official published version of this work: Aaron Bembenek, Michael Greenberg, and Stephen Chong. 2020. Formulog: Datalog for SMT-Based Static Analysis. Proc. ACM Program. Lang. 4, OOPSLA, Article 141 (November 2020), 31 pages. https://doi.org/10. 1145/3428209

Coupled Relational Symbolic Execution for Differential Privacy

Authors: Gian Pietro Farina, Stephen Chong, Marco Gaboardi

Abstract: Differential privacy is a de facto standard in data privacy with applications in the private and public sectors. Most of the techniques that achieve differential privacy are based on a judicious use of randomness. However, reasoning about randomized programs is difficult and error prone. For this reason, several techniques have been recently proposed to support designer in proving programs differe… ▽ More Differential privacy is a de facto standard in data privacy with applications in the private and public sectors. Most of the techniques that achieve differential privacy are based on a judicious use of randomness. However, reasoning about randomized programs is difficult and error prone. For this reason, several techniques have been recently proposed to support designer in proving programs differentially private or in finding violations to it. In this work we propose a technique based on symbolic execution for reasoning about differential privacy. Symbolic execution is a classic technique used for testing, counterexample generation and to prove absence of bugs. Here we use symbolic execution to support these tasks specifically for differential privacy. To achieve this goal, we leverage two ideas that have been already proven useful in formal reasoning about differential privacy: relational reasoning and probabilistic coupling. Our technique integrates these two ideas and shows how such a combination can be used to both verify and find violations to differential privacy. △ Less

Submitted 25 July, 2020; originally announced July 2020.

Quantifying the Effects of Recommendation Systems

Authors: Sunshine Chong, Andrés Abeliuk

Abstract: Recommendation systems today exert a strong influence on consumer behavior and individual perceptions of the world. By using collaborative filtering (CF) methods to create recommendations, it generates a continuous feedback loop in which user behavior becomes magnified in the algorithmic system. Popular items get recommended more frequently, creating the bias that affects and alters user preferenc… ▽ More Recommendation systems today exert a strong influence on consumer behavior and individual perceptions of the world. By using collaborative filtering (CF) methods to create recommendations, it generates a continuous feedback loop in which user behavior becomes magnified in the algorithmic system. Popular items get recommended more frequently, creating the bias that affects and alters user preferences. In order to visualize and compare the different biases, we will analyze the effects of recommendation systems and quantify the inequalities resulting from them. △ Less

Submitted 3 February, 2020; originally announced February 2020.

Comments: 8 pages, 6 figures, accepted into the National Symposium of IEEE Big Data 2019

Formalizing Privacy Laws for License Generation and Data Repository Decision Automation

Authors: Micah Altman, Stephen Chong, Alexandra Wood

Abstract: In this paper, we summarize work-in-progress on expert system support to automate some data deposit and release decisions within a data repository, and to generate custom license agreements for those data transfers. Our approach formalizes via a logic programming language the privacy-relevant aspects of laws, regulations, and best practices, supported by legal analysis documented in legal memora… ▽ More In this paper, we summarize work-in-progress on expert system support to automate some data deposit and release decisions within a data repository, and to generate custom license agreements for those data transfers. Our approach formalizes via a logic programming language the privacy-relevant aspects of laws, regulations, and best practices, supported by legal analysis documented in legal memoranda. This formalization enables automated reasoning about the conditions under which a repository can transfer data, through interrogation of users, and the application of formal rules to the facts obtained from users. The proposed system takes the specific conditions for a given data release and produces a custom data use agreement that accurately captures the relevant restrictions on data use. This enables appropriate decisions and accurate licenses, while removing the bottleneck of lawyer effort per data transfer. The operation of the system aims to be transparent, in the sense that administrators, lawyers, institutional review boards, and other interested parties can evaluate the legal reasoning and interpretation embodied in the formalization, and the specific rationale for a decision to accept or release a particular dataset. △ Less

Submitted 22 October, 2019; originally announced October 2019.

Fine-Grained, Language-Based Access Control for Database-Backed Applications

Authors: Ezra Zigmond, Stephen Chong, Christos Dimoulas, Scott Moore

Abstract: Context: Database-backed applications often run queries with more authority than necessary. Since programs can access more data than they legitimately need, flaws in security checks at the application level can enable malicious or buggy code to view or modify data in violation of intended access control policies. Inquiry: Although database management systems provide tools to control access to da… ▽ More Context: Database-backed applications often run queries with more authority than necessary. Since programs can access more data than they legitimately need, flaws in security checks at the application level can enable malicious or buggy code to view or modify data in violation of intended access control policies. Inquiry: Although database management systems provide tools to control access to data, these tools are not well-suited for modern applications which often have many users and consist of many different software components. First, databases are unaware of application users, and creating a new database user for each application user is impractical for applications with many users. Second, different components of the same application may require different authority, which would require creating different database users for different software components. Thus, it is difficult to use existing tools to properly limit the authority an application has when executing queries. For this reason, we consider a new, language-based approach to application-specific database security. Approach: Prior work has addressed the difficulty of running applications with least privilege using capability-based security and software contracts, which we adapt to the setting of database-backed applications. Knowledge: This paper's main contribution is the design and implementation of ShillDB, a language for writing secure database-backed applications. ShillDB enables reasoning about database access at the language level through capabilities, which limit which database tables a program can access, and contracts, which limit what operations a program can perform on those tables. ShillDB contracts are expressed as part of function interfaces, making it easy to specify different access control policies for different components. Contracts act as executable security documentation for ShillDB programs and are enforced by the language runtime. Further, ShillDB provides database access control guarantees independent of (and in addition to) the security mechanisms of the underlying database management system. Grounding: We have implemented a prototype of ShillDB and have used it to implement the backend for a lending library reservation system with contracts for each endpoint to evaluate the performance and usability of ShillDB. Further, we benchmark individual database operations in ShillDB to better understand the language's performance overhead. Importance: Our experience indicates that ShillDB is a practical language for enforcing database access control policies in realistic, multi-user applications and has reasonable performance overhead. ShillDB allows developers to reason about security at the component level, safely compose components, and reuse third-party components with their own application-specific database security policies. △ Less

Submitted 26 September, 2019; originally announced September 2019.

Journal ref: The Art, Science, and Engineering of Programming, 2020, Vol. 4, Issue 2, Article 3

Aquarium: Cassiopea and Alewife Languages

Authors: David A. Holland, Jingmei Hu, Ming Kawaguchi, Eric Lu, Stephen Chong, Margo I. Seltzer

Abstract: This technical report describes two of the domain specific languages used in the Aquarium kernel code synthesis project. It presents the language cores in terms of abstract syntax. Cassiopea is a machine description language for describing the semantics of processor instruction sets. Alewife is a specification language that can be used to write machine-independent specifications for assembly-level… ▽ More This technical report describes two of the domain specific languages used in the Aquarium kernel code synthesis project. It presents the language cores in terms of abstract syntax. Cassiopea is a machine description language for describing the semantics of processor instruction sets. Alewife is a specification language that can be used to write machine-independent specifications for assembly-level instruction blocks. An Alewife specification can be used to verify and synthesize code for any machine described in Cassiopea, given a machine-specific translation for abstractions used in the specification. This article does not include an introduction to either the Aquarium system or the use of the languages. In addition to this version of the article being a draft, the Aquarium project and the languages are works in progress. This article cannot currently be considered either final or complete. △ Less

Submitted 12 April, 2022; v1 submitted 31 July, 2019; originally announced August 2019.

FormuLog: Datalog for static analysis involving logical formulae

Authors: Aaron Bembenek, Stephen Chong

Abstract: Datalog has become a popular language for writing static analyses. Because Datalog is very limited, some implementations of Datalog for static analysis have extended it with new language features. However, even with these features it is hard or impossible to express a large class of analyses because they use logical formulae to represent program state. FormuLog fills this gap by extending Datalog… ▽ More Datalog has become a popular language for writing static analyses. Because Datalog is very limited, some implementations of Datalog for static analysis have extended it with new language features. However, even with these features it is hard or impossible to express a large class of analyses because they use logical formulae to represent program state. FormuLog fills this gap by extending Datalog to represent, manipulate, and reason about logical formulae. We have used FormuLog to implement declarative versions of symbolic execution and abstract model checking, analyses previously out of the scope of Datalog-based languages. While this paper focuses on the design of FormuLog and one of the analyses we have implemented in it, it also touches on a prototype implementation of the language and identifies performance optimizations that we believe will be necessary to scale FormuLog to real-world static analysis problems. △ Less

Submitted 17 September, 2018; originally announced September 2018.

Comments: Proceedings of the 11th Workshop on Answer Set Programming and Other Computing Paradigms 2018

Large-Scale Experiment on the Importance of Social Learning and Unimodality in the Wisdom of the Crowd

Authors: Dhaval Adjodah, Shi Kai Chong, Yan Leng, Peter Krafft, Alex Pentland

Abstract: In this study, we build on previous research to understand the conditions within which the Wisdom of the Crowd (WoC) improves or worsens as a result of showing individuals the predictions of their peers. Our main novel contributions are: 1) a dataset of unprecedented size and detail; 2) we observe the novel effect of the importance of the unimodality of the social information shown to individuals:… ▽ More In this study, we build on previous research to understand the conditions within which the Wisdom of the Crowd (WoC) improves or worsens as a result of showing individuals the predictions of their peers. Our main novel contributions are: 1) a dataset of unprecedented size and detail; 2) we observe the novel effect of the importance of the unimodality of the social information shown to individuals: if one does not see only one clear peak in the distribution of the crowd's predictions, the WoC is worsened after social exposure; and 3) we estimate social learning weights that we use to show that there exists individuals who are much better at learning from the crowd and can be filtered to improve collective accuracy. △ Less

Submitted 29 December, 2017; originally announced December 2017.

Social Bayesian Learning in the Wisdom of the Crowd

Authors: Dhaval Adjodah, Yan Leng, Shi Kai Chong, Peter Krafft, Alex Pentland

Abstract: Being able to correctly aggregate the beliefs of many people into a single belief is a problem fundamental to many important social, economic and political processes such as policy making, market pricing and voting. Although there exist many models and mechanisms for aggregation, there is a lack of methods and literature regarding the aggregation of opinions when influence and learning between ind… ▽ More Being able to correctly aggregate the beliefs of many people into a single belief is a problem fundamental to many important social, economic and political processes such as policy making, market pricing and voting. Although there exist many models and mechanisms for aggregation, there is a lack of methods and literature regarding the aggregation of opinions when influence and learning between individuals exist. This is in part because there are not many models of how people update their belief when exposed to the beliefs of others, and so it is hard to quantify the dependencies between people's mental models which is essential to minimizing redundancies in the aggregation. In this paper, we explore many models of how users influence and learn from each other, and we benchmark our models against the well-known DeGroot model. Our main contributions are: 1) we collect a new dataset of unprecedented size and detail to be posted online; 2) we develop a new Social Bayesian model of how people update their mental models, 3) we compare of our model to other well-known social learning models. Specifically, we show that our new Social Bayesian model is superior to the other models tested. △ Less

Submitted 28 December, 2017; originally announced December 2017.

Relational Symbolic Execution

Authors: Gian Pietro Farina, Stephen Chong, Marco Gaboardi

Abstract: Symbolic execution is a classical program analysis technique used to show that programs satisfy or violate given specifications. In this work we generalize symbolic execution to support program analysis for relational specifications in the form of relational properties - these are properties about two runs of two programs on related inputs, or about two executions of a single program on related in… ▽ More Symbolic execution is a classical program analysis technique used to show that programs satisfy or violate given specifications. In this work we generalize symbolic execution to support program analysis for relational specifications in the form of relational properties - these are properties about two runs of two programs on related inputs, or about two executions of a single program on related inputs. Relational properties are useful to formalize notions in security and privacy, and to reason about program optimizations. We design a relational symbolic execution engine, named RelSym which supports interactive refutation, as well as proving of relational properties for programs written in a language with arrays and for-like loops. △ Less

Submitted 1 August, 2019; v1 submitted 22 November, 2017; originally announced November 2017.

Cryptographically Secure Information Flow Control on Key-Value Stores

Authors: Lucas Waye, Pablo Buiras, Owen Arden, Alejandro Russo, Stephen Chong

Abstract: We present Clio, an information flow control (IFC) system that transparently incorporates cryptography to enforce confidentiality and integrity policies on untrusted storage. Clio insulates developers from explicitly manipulating keys and cryptographic primitives by leveraging the policy language of the IFC system to automatically use the appropriate keys and correct cryptographic operations. We p… ▽ More We present Clio, an information flow control (IFC) system that transparently incorporates cryptography to enforce confidentiality and integrity policies on untrusted storage. Clio insulates developers from explicitly manipulating keys and cryptographic primitives by leveraging the policy language of the IFC system to automatically use the appropriate keys and correct cryptographic operations. We prove that Clio is secure with a novel proof technique that is based on a proof style from cryptography together with standard programming languages results. We present a prototype Clio implementation and a case study that demonstrates Clio's practicality. △ Less

Submitted 29 August, 2017; originally announced August 2017.

Comments: Full version of conference paper appearing in CCS 2017

Simplified Stochastic Feedforward Neural Networks

Authors: Kimin Lee, Jaehyung Kim, Song Chong, Jinwoo Shin

Abstract: It has been believed that stochastic feedforward neural networks (SFNNs) have several advantages beyond deterministic deep neural networks (DNNs): they have more expressive power allowing multi-modal mappings and regularize better due to their stochastic nature. However, training large-scale SFNN is notoriously harder. In this paper, we aim at developing efficient training methods for SFNN, in par… ▽ More It has been believed that stochastic feedforward neural networks (SFNNs) have several advantages beyond deterministic deep neural networks (DNNs): they have more expressive power allowing multi-modal mappings and regularize better due to their stochastic nature. However, training large-scale SFNN is notoriously harder. In this paper, we aim at developing efficient training methods for SFNN, in particular using known architectures and pre-trained parameters of DNN. To this end, we propose a new intermediate stochastic model, called Simplified-SFNN, which can be built upon any baseline DNNand approximates certain SFNN by simplifying its upper latent units above stochastic ones. The main novelty of our approach is in establishing the connection between three models, i.e., DNN->Simplified-SFNN->SFNN, which naturally leads to an efficient training procedure of the stochastic models utilizing pre-trained parameters of DNN. Using several popular DNNs, we show how they can be effectively transferred to the corresponding stochastic models for both multi-modal and classification tasks on MNIST, TFD, CASIA, CIFAR-10, CIFAR-100 and SVHN datasets. In particular, we train a stochastic model of 28 layers and 36 million parameters, where training such a large-scale stochastic network is significantly challenging without using Simplified-SFNN △ Less

Submitted 11 April, 2017; originally announced April 2017.

Comments: 22 pages, 6 figures

Segmentation-free Vehicle License Plate Recognition using ConvNet-RNN

Authors: Teik Koon Cheang, Yong Shean Chong, Yong Haur Tay

Abstract: While vehicle license plate recognition (VLPR) is usually done with a sliding window approach, it can have limited performance on datasets with characters that are of variable width. This can be solved by hand-crafting algorithms to prescale the characters. While this approach can work fairly well, the recognizer is only aware of the pixels within each detector window, and fails to account for oth… ▽ More While vehicle license plate recognition (VLPR) is usually done with a sliding window approach, it can have limited performance on datasets with characters that are of variable width. This can be solved by hand-crafting algorithms to prescale the characters. While this approach can work fairly well, the recognizer is only aware of the pixels within each detector window, and fails to account for other contextual information that might be present in other parts of the image. A sliding window approach also requires training data in the form of presegmented characters, which can be more difficult to obtain. In this paper, we propose a unified ConvNet-RNN model to recognize real-world captured license plate photographs. By using a Convolutional Neural Network (ConvNet) to perform feature extraction and using a Recurrent Neural Network (RNN) for sequencing, we address the problem of sliding window approaches being unable to access the context of the entire image by feeding the entire image as input to the ConvNet. This has the added benefit of being able to perform end-to-end training of the entire model on labelled, full license plate images. Experimental results comparing the ConvNet-RNN architecture to a sliding window-based approach shows that the ConvNet-RNN architecture performs significantly better. △ Less

Submitted 23 January, 2017; originally announced January 2017.

Comments: 5 pages, 3 figures, International Workshop on Advanced Image Technology, January, 8-10, 2017. Penang, Malaysia. Proceeding IWAIT2017

ACM Class: I.4.0, I.5.1, I.5.4, I.7.5

Abnormal Event Detection in Videos using Spatiotemporal Autoencoder

Authors: Yong Shean Chong, Yong Haur Tay

Abstract: We present an efficient method for detecting anomalies in videos. Recent applications of convolutional neural networks have shown promises of convolutional layers for object detection and recognition, especially in images. However, convolutional neural networks are supervised and require labels as learning signals. We propose a spatiotemporal architecture for anomaly detection in videos including… ▽ More We present an efficient method for detecting anomalies in videos. Recent applications of convolutional neural networks have shown promises of convolutional layers for object detection and recognition, especially in images. However, convolutional neural networks are supervised and require labels as learning signals. We propose a spatiotemporal architecture for anomaly detection in videos including crowded scenes. Our architecture includes two main components, one for spatial feature representation, and one for learning the temporal evolution of the spatial features. Experimental results on Avenue, Subway and UCSD benchmarks confirm that the detection accuracy of our method is comparable to state-of-the-art methods at a considerable speed of up to 140 fps. △ Less

Submitted 6 January, 2017; originally announced January 2017.

Report on the NSF Workshop on Formal Methods for Security

Authors: Stephen Chong, Joshua Guttman, Anupam Datta, Andrew Myers, Benjamin Pierce, Patrick Schaumont, Tim Sherwood, Nickolai Zeldovich

Abstract: Report on the NSF Workshop on Formal Methods for Security, held 19-20 November 2015. Report on the NSF Workshop on Formal Methods for Security, held 19-20 November 2015. △ Less

Submitted 3 August, 2016; v1 submitted 1 August, 2016; originally announced August 2016.

Vulnerability of linear systems against sensor attacks--a system's security index

Authors: Michelle S. Chong, Margreta Kuijper

Abstract: The `security index' of a discrete-time LTI system under sensor attacks is introduced as a quantitative measure on the security of an observable system. We derive ideas from error control coding theory to provide sufficient conditions for attack detection and correction. The `security index' of a discrete-time LTI system under sensor attacks is introduced as a quantitative measure on the security of an observable system. We derive ideas from error control coding theory to provide sufficient conditions for attack detection and correction. △ Less

Submitted 21 February, 2016; originally announced February 2016.

Comments: Submitted

MSC Class: 93B35; 94B05

Journal ref: Proceedings of MTNS 2016 (International Symposium on Mathematical Theory of Networks and Systems, July 2016, Minneapolis, USA), pp.373-376

Precise, Dynamic Information Flow for Database-Backed Applications

Authors: Jean Yang, Travis Hance, Thomas H. Austin, Armando Solar-Lezama, Cormac Flanagan, Stephen Chong

Abstract: We present an approach for dynamic information flow control across the application and database. Our approach reduces the amount of policy code required, yields formal guarantees across the application and database, works with existing relational database implementations, and scales for realistic applications. In this paper, we present a programming model that factors out information flow policies… ▽ More We present an approach for dynamic information flow control across the application and database. Our approach reduces the amount of policy code required, yields formal guarantees across the application and database, works with existing relational database implementations, and scales for realistic applications. In this paper, we present a programming model that factors out information flow policies from application code and database queries, a dynamic semantics for the underlying λ^JDB core language, and proofs of termination-insensitive non-interference and policy compliance for the semantics. We implement these ideas in Jacqueline, a Python web framework, and demonstrate feasibility through three application case studies: a course manager, a health record system, and a conference management system used to run an academic workshop. We show that in comparison to traditional applications with hand-coded policy checks, Jacqueline applications have 1) a smaller trusted computing base, 2) fewer lines of policy code, and 2) reasonable, often negligible, additional overheads. △ Less

Submitted 23 April, 2016; v1 submitted 13 July, 2015; originally announced July 2015.

ACM Class: D.3.3

Modeling Representation of Videos for Anomaly Detection using Deep Learning: A Review

Authors: Yong Shean Chong, Yong Haur Tay

Abstract: This review article surveys the current progresses made toward video-based anomaly detection. We address the most fundamental aspect for video anomaly detection, that is, video feature representation. Much research works have been done in finding the right representation to perform anomaly detection in video streams accurately with an acceptable false alarm rate. However, this is very challenging… ▽ More This review article surveys the current progresses made toward video-based anomaly detection. We address the most fundamental aspect for video anomaly detection, that is, video feature representation. Much research works have been done in finding the right representation to perform anomaly detection in video streams accurately with an acceptable false alarm rate. However, this is very challenging due to large variations in environment and human movement, and high space-time complexity due to huge dimensionality of video data. The weakly supervised nature of deep learning algorithms can help in learning representations from the video data itself instead of manually designing the right feature for specific scenes. In this paper, we would like to review the existing methods of modeling video representations using deep learning techniques for the task of anomaly detection and action recognition. △ Less

Submitted 4 May, 2015; originally announced May 2015.

Comments: arXiv admin note: text overlap with arXiv:1411.4423 by other authors

Using Architecture to Reason about Information Security

Authors: Stephen Chong, Ron van der Meyden

Abstract: We demonstrate, by a number of examples, that information-flow security properties can be proved from abstract architectural descriptions, that describe only the causal structure of a system and local properties of trusted components. We specify these architectural descriptions of systems by generalizing intransitive noninterference policies to admit the ability to filter information passed betwee… ▽ More We demonstrate, by a number of examples, that information-flow security properties can be proved from abstract architectural descriptions, that describe only the causal structure of a system and local properties of trusted components. We specify these architectural descriptions of systems by generalizing intransitive noninterference policies to admit the ability to filter information passed between communicating domains. A notion of refinement of such system architectures is developed that supports top-down development of architectural specifications and proofs by abstraction of information security properties. We also show that, in a concrete setting where the causal structure is enforced by access control, a static check of the access control setting plus local verification of the trusted components is sufficient to prove that a generalized intransitive noninterference policy is satisfied. △ Less

Submitted 1 September, 2014; originally announced September 2014.

Delay-Optimal Data Forwarding in Vehicular Sensor Networks

Authors: Okyoung Choi, Seokhyun Kim, Jaeseong Jeong, Hyang-Won Lee, Song Chong

Abstract: Vehicular Sensor Network (VSN) is emerging as a new solution for monitoring urban environments such as Intelligent Transportation Systems and air pollution. One of the crucial factors that determine the service quality of urban monitoring applications is the delivery delay of sensing data packets in the VSN. In this paper, we study the problem of routing data packets with minimum delay in the VSN,… ▽ More Vehicular Sensor Network (VSN) is emerging as a new solution for monitoring urban environments such as Intelligent Transportation Systems and air pollution. One of the crucial factors that determine the service quality of urban monitoring applications is the delivery delay of sensing data packets in the VSN. In this paper, we study the problem of routing data packets with minimum delay in the VSN, by exploiting i) vehicle traffic statistics, ii) anycast routing and iii) knowledge of future trajectories of vehicles such as buses. We first introduce a novel road network graph model that incorporates the three factors into the routing metric. We then characterize the packet delay on each edge as a function of the vehicle density, speed and the length of the edge. Based on the network model and delay function, we formulate the packet routing problem as a Markov Decision Process (MDP) and develop an optimal routing policy by solving the MDP. Evaluations using real vehicle traces in a city show that our routing policy significantly improves the delay performance compared to existing routing protocols. △ Less

Submitted 20 September, 2012; originally announced September 2012.

Economics of WiFi Offloading: Trading Delay for Cellular Capacity

Authors: Joohyun Lee, Yung Yi, Song Chong, Youngmi Jin

Abstract: Cellular networks are facing severe traffic overloads due to the proliferation of smart handheld devices and traffic-hungry applications. A cost-effective and practical solution is to offload cellular data through WiFi. Recent theoretical and experimental studies show that a scheme, referred to as delayed WiFi offloading, can significantly save the cellular capacity by delaying users' data and exp… ▽ More Cellular networks are facing severe traffic overloads due to the proliferation of smart handheld devices and traffic-hungry applications. A cost-effective and practical solution is to offload cellular data through WiFi. Recent theoretical and experimental studies show that a scheme, referred to as delayed WiFi offloading, can significantly save the cellular capacity by delaying users' data and exploiting mobility and thus increasing chance of meeting WiFi APs (Access Points). Despite a huge potential of WiFi offloading in alleviating mobile data explosion, its success largely depends on the economic incentives provided to users and operators to deploy and use delayed offloading. In this paper, we study how much economic benefits can be generated due to delayed WiFi offloading, by modeling a market based on a two-stage sequential game between a monopoly provider and users. We also provide extensive numerical results computed using a set of parameters from the real traces and Cisco's projection of traffic statistics in year 2015. In both analytical and numerical results, we model a variety of practical scenarios and control knobs in terms of traffic demand and willingness to pay of users, spatio-temporal dependence of pricing and traffic, and diverse pricing and delay tolerance. We demonstrate that delayed WiFi offloading has considerable economic benefits, where the increase ranges from 21% to 152% in the provider's revenue, and from 73% to 319% in the users' surplus, compared to on-the-spot WiFi offloading. △ Less

Submitted 31 December, 2012; v1 submitted 27 July, 2012; originally announced July 2012.

Comments: 15 pages, 11 figures, submitted for publication

Making 802.11 DCF Optimal: Design, Implementation, and Evaluation

Authors: Jinsung Lee, Yung Yi, Song Chong, Bruno Nardelli, Edward W. Knightly, Mung Chiang

Abstract: This paper proposes a new protocol called Optimal DCF (O-DCF). Inspired by a sequence of analytic results, O-DCF modifies the rule of adapting CSMA parameters, such as backoff time and transmission length, based on a function of the demand-supply differential of link capacity captured by the local queue length. Unlike clean-slate design, O-DCF is fully compatible with 802.11 hardware, so that it c… ▽ More This paper proposes a new protocol called Optimal DCF (O-DCF). Inspired by a sequence of analytic results, O-DCF modifies the rule of adapting CSMA parameters, such as backoff time and transmission length, based on a function of the demand-supply differential of link capacity captured by the local queue length. Unlike clean-slate design, O-DCF is fully compatible with 802.11 hardware, so that it can be easily implemented only with a simple device driver update. Through extensive simulations and real experiments with a 16-node wireless network testbed, we evaluate the performance of O-DCF and show that it achieves near-optimality, and outperforms other competitive ones, such as 802.11 DCF, optimal CSMA, and DiffQ in a wide range of scenarios. △ Less

Submitted 7 July, 2012; originally announced July 2012.

Comments: 13 pages, 16 figures, submitted for publication

MSC Class: 68-06 ACM Class: C.2.1

On the Generalized Delay-Capacity Tradeoff of Mobile Networks with Lévy Flight Mobility

Authors: Yoora Kim, Kyunghan Lee, Ness B. Shroff, Injong Rhee, Song Chong

Abstract: In the literature, scaling laws for wireless mobile networks have been characterized under various models of node mobility and several assumptions on how communication occurs between nodes. To improve the realism in the analysis of scaling laws, we propose a new analytical framework. The framework is the first to consider a Lévy flight mobility pattern, which is known to closely mimic human mobili… ▽ More In the literature, scaling laws for wireless mobile networks have been characterized under various models of node mobility and several assumptions on how communication occurs between nodes. To improve the realism in the analysis of scaling laws, we propose a new analytical framework. The framework is the first to consider a Lévy flight mobility pattern, which is known to closely mimic human mobility patterns. Also, this is the first work that allows nodes to communicate while being mobile. Under this framework, delays ($\bar{D}$) to obtain various levels of per-node throughput $(λ)$ for Lévy flight are suggested as $\bar{D}(λ) = O(\sqrt{\min (n^{1+α} λ, n^2)})$, where Lévy flight is a random walk of a power-law flight distribution with an exponent $α\in (0,2]$. The same framework presents a new tighter tradeoff $\bar{D}(λ) = O(\sqrt{\max (1,nλ^3)})$ for \textit{i.i.d.} mobility, whose delays are lower than existing results for the same levels of per-node throughput. △ Less

Submitted 6 July, 2012; originally announced July 2012.

Comments: 21 pages

Truthful Mechanisms for Agents that Value Privacy

Authors: Yiling Chen, Stephen Chong, Ian A. Kash, Tal Moran, Salil Vadhan

Abstract: Recent work has constructed economic mechanisms that are both truthful and differentially private. In these mechanisms, privacy is treated separately from the truthfulness; it is not incorporated in players' utility functions (and doing so has been shown to lead to non-truthfulness in some cases). In this work, we propose a new, general way of modelling privacy in players' utility functions. Speci… ▽ More Recent work has constructed economic mechanisms that are both truthful and differentially private. In these mechanisms, privacy is treated separately from the truthfulness; it is not incorporated in players' utility functions (and doing so has been shown to lead to non-truthfulness in some cases). In this work, we propose a new, general way of modelling privacy in players' utility functions. Specifically, we only assume that if an outcome $o$ has the property that any report of player $i$ would have led to $o$ with approximately the same probability, then $o$ has small privacy cost to player $i$. We give three mechanisms that are truthful with respect to our modelling of privacy: for an election between two candidates, for a discrete version of the facility location problem, and for a general social choice problem with discrete utilities (via a VCG-like mechanism). As the number $n$ of players increases, the social welfare achieved by our mechanisms approaches optimal (as a fraction of $n$). △ Less

Submitted 13 November, 2012; v1 submitted 23 November, 2011; originally announced November 2011.

On the Critical Delays of Mobile Networks under Lévy Walks and Lévy Flights

Authors: Kyunghan Lee, Yoora Kim, Song Chong, Injong Rhee, Yung Yi, Ness. B. Shroff

Abstract: Delay-capacity tradeoffs for mobile networks have been analyzed through a number of research work. However, Lévy mobility known to closely capture human movement patterns has not been adopted in such work. Understanding the delay-capacity tradeoff for a network with Lévy mobility can provide important insights into understanding the performance of real mobile networks governed by human mobility. T… ▽ More Delay-capacity tradeoffs for mobile networks have been analyzed through a number of research work. However, Lévy mobility known to closely capture human movement patterns has not been adopted in such work. Understanding the delay-capacity tradeoff for a network with Lévy mobility can provide important insights into understanding the performance of real mobile networks governed by human mobility. This paper analytically derives an important point in the delay-capacity tradeoff for Lévy mobility, known as the critical delay. The critical delay is the minimum delay required to achieve greater throughput than what conventional static networks can possibly achieve (i.e., $O(1/\sqrt{n})$ per node in a network with $n$ nodes). The Lévy mobility includes Lévy flight and Lévy walk whose step size distributions parametrized by $α\in (0,2]$ are both heavy-tailed while their times taken for the same step size are different. Our proposed technique involves (i) analyzing the joint spatio-temporal probability density function of a time-varying location of a node for Lévy flight and (ii) characterizing an embedded Markov process in Lévy walk which is a semi-Markov process. The results indicate that in Lévy walk, there is a phase transition such that for $α\in (0,1)$, the critical delay is always $Θ(n^{1/2})$ and for $α\in [1,2]$ it is $Θ(n^{\fracα{2}})$. In contrast, Lévy flight has the critical delay $Θ(n^{\fracα{2}})$ for $α\in(0,2]$. △ Less

Submitted 1 February, 2012; v1 submitted 20 November, 2011; originally announced November 2011.

REFIM: A Practical Interference Management in Heterogeneous Wireless Access Networks

Authors: Kyuho Son, Soohwan Lee, Yung Yi, Song Chong

Abstract: Due to the increasing demand of capacity in wireless cellular networks, the small cells such as pico and femto cells are becoming more popular to enjoy a spatial reuse gain, and thus cells with different sizes are expected to coexist in a complex manner. In such a heterogeneous environment, the role of interference management (IM) becomes of more importance, but technical challenges also increase,… ▽ More Due to the increasing demand of capacity in wireless cellular networks, the small cells such as pico and femto cells are becoming more popular to enjoy a spatial reuse gain, and thus cells with different sizes are expected to coexist in a complex manner. In such a heterogeneous environment, the role of interference management (IM) becomes of more importance, but technical challenges also increase, since the number of cell-edge users, suffering from severe interference from the neighboring cells, will naturally grow. In order to overcome low performance and/or high complexity of existing static and other dynamic IM algorithms, we propose a novel low-complex and fully distributed IM scheme, called REFIM, in the downlink of heterogeneous multi-cell networks. We first formulate a general optimization problem that turns out to require intractable computation complexity for global optimality. To have a practical solution with low computational and signaling overhead, which is crucial for low-cost small-cell solutions, e.g., femto cells, in REFIM, we decompose it into per-BS problems based on the notion of reference user and reduce feedback overhead over backhauls both temporally and spatially. We evaluate REFIM through extensive simulations under various configurations, including the scenarios from a real deployment of BSs. We show that, compared to the schemes without IM, REFIM can yield more than 40% throughput improvement of cell-edge users while increasing the overall performance by 10~107%. This is equal to about 95% performance of the existing centralized IM algorithm that is known to be near-optimal but hard to implement in practice due to prohibitive complexity. We also present that as long as interference is managed well, the spectrum sharing policy can outperform the best spectrum splitting policy where the number of subchannels is optimally divided between macro and femto cells. △ Less

Submitted 4 May, 2011; originally announced May 2011.

Comments: 13 pages

A Framework for Creating Natural Language User Interfaces for Action-Based Applications

Authors: Stephen Chong, Riccardo Pucella

Abstract: In this paper we present a framework for creating natural language interfaces to action-based applications. Our framework uses a number of reusable application-independent components, in order to reduce the effort of creating a natural language interface for a given application. Using a type-logical grammar, we first translate natural language sentences into expressions in an extended higher-ord… ▽ More In this paper we present a framework for creating natural language interfaces to action-based applications. Our framework uses a number of reusable application-independent components, in order to reduce the effort of creating a natural language interface for a given application. Using a type-logical grammar, we first translate natural language sentences into expressions in an extended higher-order logic. These expressions can be seen as executable specifications corresponding to the original sentences. The executable specifications are then interpreted by invoking appropriate procedures provided by the application for which a natural language interface is being created. △ Less

Submitted 16 December, 2004; originally announced December 2004.

Comments: 25 pages, 1 figure. A preliminary version of this paper appeared in the Proceedings of the Third International AMAST Workshop on Algebraic Methods in Language Processing, TWLT Report 21, pp. 83-98, 2003

ACM Class: H.5.2; I.2.7; F.4.2; F.4.1