Interactive user experiences on the web are becoming the norm. Client-side programs are becoming more complicated and have to deal with event handling, reading HTML document state and updating the interface. In this paper we propose a declarative language that supports these three facets of client-side browser development declaratively and provides a programming model where complex interfaces can be written using simple programming techniques such as records, functions and recursion.
The polymorphic RPC calculus allows programmers to write succinct multitier programs using polymorphic location constructs. However, until now it lacked an implementation. We develop an experimental programming language based on the polymorphic RPC calculus. We introduce a polymorphic Client-Server (CS) calculus with the client and server parts separated. In contrast to existing untyped CS calculi, our calculus is not only able to resolve polymorphic locations statically, but it is also able to do so dynamically. We design a type-based slicing compilation of the polymorphic RPC calculus into this CS calculus, proving type and semantic correctness. We propose a method to erase types unnecessary for execution but retaining locations at runtime by translating the polymorphic CS calculus into an untyped CS calculus, proving semantic correctness.
The RPC calculus is a simple semantic foundation for multi-tier programming languages such as Links in which located functions can be written for the client-server model. Subsequently, the typed RPC calculus is designed to capture the location information of functions by types and to drive location type-directed slicing compilations. However, the use of locations is currently limited to monomorphic ones, which is one of the gaps to overcome to put into practice the theory of RPC calculi for client-server model. This paper proposes a polymorphic RPC calculus to allow programmers to write succinct multi-tier programs using polymorphic location constructs. Then the polymorphic multi-tier programs can be automatically translated into programs only containing location constants amenable to the existing slicing compilation methods. We formulate a type system for the polymorphic RPC calculus, and prove its type soundness. Also, we design a monomorphization translation together with proofs on its type and semantic correctness for the translation.
With multi-tier programming languages, programmers can specify the locations of code to run in order to reduce development efforts for the web-based client-server model where programmers write client and server programs separately and test the multiple programs together. The RPC calculus, one of the foundations of those languages by Cooper and Wadler, has the feature of symmetric communication in programmer's writing arbitrarily deep nested client-server interactions. However, the existing research only considers dynamically typed locations. We propose a typed RPC calculus where locations are tracked in type-level. A new located type system paves the way for a theory of RPC calculi for the client-server model.
(In the following papers published in SCP2020 and PPDP2021, the typed RPC calculus will be enhanced with polymorphic locations and a type-based slicing compilation.)
This paper presents a text-based syntax completion method that uses an LR parser. We propose formal definitions of candidate text to be completed based on the sentential forms. Moreover, we design basic algorithms for computing candidate texts through reductions in the LR parsing. This is unlike most existing methods, wherein the definition of candidates that are intended to be generated are given informally. In addition, this is unlike grammar transformation approaches that use LR parsers and is a currently burdensome task. The proposed method allows LR parsers to be adopted without modification and a syntax completion system to be built without incurring efforts. For practical purposes, we extended the basic algorithms using a new definition of refined candidates and a new strategy. The extended algorithms can compute more useful candidates for realistic programming language grammars than those of existing ones; Further, we implemented the algorithms on an Emacs server to demonstrate the feasibility of their application. We evaluated the extended algorithm with three real-world programming languages, Small Basic, C, and Haskell. The extended algorithm computes half of all candidates in less than or equal to 0.2 seconds and 89.2\% in approximately one second in the evaluation while computing the remaining candidates took a long time. We discuss its evaluation in detail.
This paper presents a text-based syntax completion method using an LR parser. We propose formal definitions of candidate text to be completed based on the sentential forms, and we design algorithms for computing candidates through reductions in the LR parsing. This is in contrast to the existing methods that have not clearly stated what candidates they intend to produce. This is also different from a transformation approach using an LR parser, which transforms the grammar of the programming language, a burdensome task at this moment. The advantage of our method is that LR parsers can be adopted without modification, and a syntax completion system can be built using them, without incurring efforts. We implemented the algorithms as an Emacs server to demonstrate the feasibility of their application.
본 논문은 LR 파서를 쉽게 개발하기 위하여 두 가지 아이디어를 제안한다. 첫째, 오토마타 생 성을 모듈화하여 새로운 프로그래밍 언어를 위한 파서 생성 도구를 쉽게 개발 할 수 있다. 둘째, 파서 명 세를 일반 프로그래밍언어로 작성하도록 구성하여 이 언어 개발 환경에서 제공하는 구문 오류, 자동 완성, 타입 오류 검사 기능들을 이용하여 파서 명세의 오류를 바로잡을 수 있다. 이 연구에서 제안한 아이디어 로 Python, Java, C++, Haskell로 파서를 작성할 수 있는 도구를 개발하였고, 실험을 통하여 위 두 가지 장점을 보였다.
This paper proposes two ways to develop LR parsers easily. First, one can write a parser specification in a general programming language and derive the benefits of syntax error checking, code completion, and type-error checking over the specification from the language’s development environment. Second, to make it easy to develop a parser tool for a new programming language, the automata generation for the parser specifications is in a modular form. With the idea proposed in this study, we developed a tool for writing parsers in Python, Java, C++, and Haskell. We also demonstrated the two aforementioned advantages in an experiment.
Internet of things (IoT) applications called SmartApps are event-driven programs running on the SmartThings cloud. To understand the behaviour of SmartApps, users may have questions regarding which execution flows follow particular events or why specific actions occur. However, checking internal programme behaviours, such as event-driven execution flows, is more difficult for users because SmartApps run on the cloud. In this paper, we propose SmartProvenance, which is a provenance system for IoT applications and provides a graphical user interface (GUI) environment for provenance queries on event flow graphs. The event flow graph of a SmartApp visualises all execution control flows initiated by events, which are constructed by performing static programme analysis. The graph is decorated with dynamically collected event and action information in the GUI interface for provenance queries. Then, users can query the provenance by simply clicking on the graph. An event flow graph as the form of a GUI for queries in the SmartProvenance system allows users to view IoT services by all possible event flow paths in a SmartApp. Thus, the provenance information being visualised on the event flow graph can be intuitively understood in the context of IoT services. Therefore, users can answer provenance questions themselves without difficulty.
A visual block programming language allows users to make their own programs by dragging and dropping graphic blocks rather than by writing the program. This enables users who are not proficient in programming to create programs easily. Although existing studies have applied this idea to programming Internet of things (IoT) applications, existing visual language tools have certain limitations in terms of expressiveness, extensibility, and error prevention. In this paper, we propose a visual block language called Smart Block for SmartThings home automation, together with a visual programming environment that supports the three properties. We designed the visual block language based on the Internet of things automation (IoTa) calculus, a core calculus for IoT automation that generalizes event-condition-action (ECA) rules. Each ECA rule specifies that when an event occurs, and if a condition is met, a certain action is performed. Smart Block supports writing IoT applications in the ECA style and is implemented with Google Blockly, a client-side JavaScript library for creating visual block languages. Smart Block can help users develop reliable SmartApps by checking for redundancy, inconsistency, and circularity in the ECA rules before generating the code. We demonstrate that Smart Block can build 54 out of 56 (96.4%) of the SmartApps provided by the official SmartThings IDE. Furthermore, a user study with 33 participants shows that our approach, based on the foundation of the IoTa calculus, is understandable for users.
SmartThings is one of the most widely used smart home platforms for the internet of things (IoT). SmartApps are IoT applications on the SmartThings platform that enables automation of home devices. SmartApps are event-driven; inputs are received from device events, and outputs are issued to control devices. Understanding the behaviour of IoT applications is a challenge because the inputs and outputs are rarely visible. To tackle the challenge, the proposed approach is to visualise IoT applications as a set of IoT services. The authors propose an event-flow-based visualisation method where a flow from an event to action is viewed as an IoT service. The authors implement a tool called SmartVisual that performs a static analysis on SmartApps to generate a diagram of event flows. The tool also provides a tree model of the static structure of SmartApps and software metrics relevant to the event-driven nature. The tool was applied to 64 SmartApp samples provided by SmartThings. Each SmartApp had four event flows on average, although the most complex SmartApp had 58 event flows, and two inputs and two outputs, and the average length of the event flows was 1.43 methods.
본 연구에서는 웹 취약점 스캐너의 복잡한 취약점 탐지 성능을 향상시키기 위해 그래머 퍼저를 활용하고자 한다. 이를 위해 그래머 퍼저를 사용한 페이로드를 생성 방법론을 제시하였고, 그래머 퍼징을 적용한 웹 취약점 스캐너인 웹 퍼저를 개발했다. 추가적으로 효과적인 웹 취약점 탐지를 위해 크롤링, 비동기, 병렬 처리의 중요성을 강조했다.
다계층 프로그래밍 언어(Multi-tier programming language)란 시스템의 각
계층의 구성 요소를 같은 컴파일 단위로 혼합해 개발과정 중 오류가
발생하기 쉬운 단점을 개선하기 위해 제안된 언어이다. 그 결과 각 계층을
개발할 때 발생할 수 있는 오류를 줄이는 장점이 있다. 그러나 현재까지
다계층 프로그래밍 언어로 작성한 웹 프로그램의 취약점을 분석하는 연구가
없었다. 이러한 다계층 프로그래밍 언어의 한 종류인 Links로 작성된
프로그램을 대상으로 Links 프로그램의 웹 취약점을 분석한 결과를 리포트
한다.
(이 논문은 OWASP ZAP을 이용한 다계층 프로그래밍 언어 Links의 웹 취약점 분석(이규해, 창병모, 최광훈, 한국소프트웨어종합학술대회-KSC2021, 2021년 12월20일-22일) 포스터 논문을 확장한 구두 발표 논문임)
자체 수정 코드(Self-Modifying-Code)란 실행 시간 동안 스스로 실행 코드를 변경하는 코드를 말한다. 이런 기법은 특히 악성코드가 정적 분석을 우회하는 데 악용된다. 따라서 이러한 악성코드를 효과적으로 검출하려면 자체 수정 코드를 파악하는 것이 중요하다. 그동안 동적 분석 방법으로 자체 수정 코드를 분석해왔으나 이는 시간과 비용이 많이 든다. 만약 정적 분석으로 자체 수정 코드를 검출할 수 있다면 악성코드 분석에 큰 도움이 될 것이다. 본 논문에서는 LLVM IR로 변환한 바이너리 실행 프로그램을 대상으로 자체 수정 코드를 탐지하는 정적 분석방법을 제안하고, 자체 수정 코드 벤치마크를 만들어 이 방법을 적용했다. 본 논문의 실험 결과 벤치마크 프로그램을 컴파일로 변환한 최적화된 형태의 LLVM IR 프로그램에 대해서는 설계한 정적 분석 방법이 효과적이었다. 하지만 바이너리를 리프팅 변환한 비정형화된 LLVM IR 프로그램에 대해서는 자체 수정 코드를 검출하기 어려운 한계가 있었다. 이를 극복하기 위해 바이너리를 리프팅 하는 효과적인 방법이 필요하다.
Self-Modifying-Code is a code that changes the code by itself during execution time. This technique is particularly abused by malicious code to bypass static analysis. Therefor, in order to effectively detect such malicious codes, it is important to identify self-modifying-codes. In the meantime, Self-modify-codes have been analyzed using dynamic analysis methods, but this is time-consuming and costly. If static analysis can detect self-modifying-code it will be of great help to malicious code analysis. In this paper, we propose a static analysis method to detect self-modified code for binary executable programs converted to LLVM IR and apply this method by making a self-modifying-code benchmark. As a result of the experiment in this paper, the designed static analysis method was effective for the standardized LLVM IR program that was compiled and converted to the benchmark program. However, there was a limitation in that it was difficult to detect the self-modifying-code for the unstructured LLVM IR program in which the binary was lifted and transformed. To overcome this, we need an effective way to lift the binary code.
SmartThings is one of the most popular open platforms for home automation IoT solutions that allows users to create their own applications called SmartApps for personal use or for public distribution. The nature of openness demands high standards on the quality of SmartApps, but there have been few studies that have evaluated this thoroughly yet. As part of software quality practice, code reviews are responsible for detecting violations of coding standards and ensuring that best practices are followed. The purpose of this research is to propose systematically designed quality metrics under the well-known Goal/Question/Metric methodology and to evaluate the quality of SmartApps through automatic code reviews using a static analysis. We first organize our static analysis rules by following the GQM methodology, and then we apply the rules to real-world SmartApps to analyze and evaluate them. A study of 105 officially published and 74 community-created real-world SmartApps found a high ratio of violations in both types of SmartApps, and of all violations, security violations were most common. Our static analysis tool can effectively inspect reliability, maintainability, and security violations. The results of the automatic code review indicate the common violations among SmartApps.
This research aims at a new practical Intent fuzzing tool for detecting Intent vulnerabilities of Android apps causing the robustness problem. We proposed two new ideas. First, we designed an Intent specification language to describe the structure of Intent, which makes our Intent fuzz testing tool flexible. Second, we proposed an automatic tally method classifying unique failures. With the two ideas, we implemented an Intent fuzz testing tool called Hwacha, and evaluated it with 50 commercial Android apps. Our tool offers an arbitrary combination of automatic and manual Intent generators with executors such as ADB and JUnit due to the use of the Intent specification language. The automatic tally method excluded almost 80% of duplicate failures in our experiment, reducing efforts of testers very much in review of failures. The tool uncovered more than 400 unique failures including what is unknown so far. We also measured execution time for Intent fuzz testing, which has been rarely reported before. Our tool is practical because the whole procedure of fuzz testing is fully automatic and the tool is applicable to the large number of Android apps with no human intervention.
사물 인터넷 환경에서 모바일 어플리케이션과 웨어러블 기기를 연동하기 위해 BLE (Bluetooth Low Energy) 기반 통신을 많이 활용하고 있다. 특히 BLE 연동 안드로이드 어플리케이션을 개발할 때 개발 환경에서 BLE 에뮬레이션을 지원하지 않아 반드시 웨어러블 기기가 필요한 제약이 있 다. 본 연구에서는 처음으로 안드로이드 BLE 에뮬레이터를 설계 및 구현하였다. 이를 활용하여 웨어러블 기기가 없어도 BLE 연동 어플리케이션을 개발할 수 있음을 확인하였다. 그리고 그래프 모델 기반의 안 드로이드 BLE 시나리오 자동 생성 방법을 제안하고 자동 생성한 시나리오들을 제안한 안드로이드 BLE 에뮬레이터 상에서 실행하여 어플리케이션의 BLE 응용 프로토콜을 체계적으로 테스트하는데 유용함을 보였다.
BLE (Bluetooth Low Energy) has been extensively used for communication between mobile applications and wearable devices in IoT (Internet of Things). In developing Android applications, wearable devices, on which the applications can run, should be available because the existing Android SDK does not support any BLE emulation facility. In this study, we have designed and implemented the first Android BLE emulator. Using this, we are able to develop and test BLE-based Android applications even when without wearable devices. We have also proposed an automatic generation method of Android BLE scenarios based on graph model. We have shown that the method is useful for systematically testing BLE application protocols by running the generated scenarios on the Android BLE emulator.
Recent researches have reported that Android programs are vulnerable to unexpected exceptions. One reason is that the current design of Android platform solely depends on Java exception mechanism, which is unaware of the component-based structure of Android programs. This paper proposes a component-level exception mechanism for programmers to build robust Android programs with. With the mechanism, they can define an intra-component handler for each component to recover from exceptions, and they can propagate uncaught exceptions to caller component along the reverse of component activation flow. Theoretically, we have formalized an Android semantics with exceptions to prove the robustness property of the mechanism. In practice, we have implemented the mechanism with a domain-specific library that extends existing Android components. This lightweight approach does not demand the change of the Android platform. In our experiment with Android benchmark programs, the library is found to catch a number of runtime exceptions that would otherwise get the programs terminated abnormally. We also measure the overhead of using the library to show that it is very small. Our proposal is a new mechanism for defending Android programs from unexpected exceptions.
안드로이드 기반 스마트폰 앱의 바이너리 코드를 오프라인 상에서 분석하여 유해 사이트 목록에 포함된 서버에 접속하는지 여부를판단하는 시스템을 제안하고, 실제 앱에 대해 적용한 실험 결과를 제시한다. 주어진 앱의 바이너리 코드를 Java 바이트 코드로 역 컴파일하고, 문자열분석을 적용하여 프로그램에서 사용하는 모든 문자열 집합을 계산한 다음, 유해 매체물을 제공하는 사이트 URL을 포함하는지 확인하는방법이다. 이 시스템은 앱을 실행하지 않고 배포 단계에서 검사할 수 있고 앱 마켓 관리에서 유해 사이트를 접속하는 앱을 분류하는 작업을자동화할 수 있는 장점이 있다. DNS 서버를 이용하거나 스마트폰에 모니터링 모듈을 설치하여 차단하는 기존 방법들과 서로 다른 단계에서유해앱을 차단함으로써 상호 보완할 수 있는 방법이 될 수 있다.
This paper proposes a method of forgery protection and user’s dynamic access control in NFC standards compliant program messages. We implement this proposal in Android phones to test mobile applicability. The sizes of benchmark program messages are small enough to be stored in stock NFC tags, and the total execution time increased due to employing the two security methods is not noticeable to users in NFC service.
안드로이드 기반 스마트폰 앱의 바이너리 코드를 오프라인 상에서 분석하여 유해 사이트 목록에 포함된 서버에 접속하는지 여부를판단하는 시스템을 제안하고, 실제 앱에 대해 적용한 실험 결과를 제시한다. 주어진 앱의 바이너리 코드를 Java 바이트 코드로 역 컴파일하고, 문자열분석을 적용하여 프로그램에서 사용하는 모든 문자열 집합을 계산한 다음, 유해 매체물을 제공하는 사이트 URL을 포함하는지 확인하는방법이다. 이 시스템은 앱을 실행하지 않고 배포 단계에서 검사할 수 있고 앱 마켓 관리에서 유해 사이트를 접속하는 앱을 분류하는 작업을자동화할 수 있는 장점이 있다. DNS 서버를 이용하거나 스마트폰에 모니터링 모듈을 설치하여 차단하는 기존 방법들과 서로 다른 단계에서유해앱을 차단함으로써 상호 보완할 수 있는 방법이 될 수 있다.
This paper proposes a string analysis based system for classifying Android Apps that may access so called harmful sites, and shows an experiment result for real Android apps on the market. The system first transforms Android App binary codes into Java byte codes, it performs string analysis to compute a set of strings at all program points, and it classifies the Android App as bad ones if the computed set contains URLs that are classified because the sites provide inappropriate contents. In the proposed approach, the system performs such a classification in the stage of distribution before installing and executing the Apps. Furthermore, the system is suitable for the automatic management of Android Apps in the market. The proposed system can be combined with the existing methods using DNS servers or monitoring modules to identify harmful Android apps better in different stages.
본 연구에서는 웹 취약점 스캐너의 복잡한 취약점 탐지 성능을 향상시키기 위해 그래머 퍼저 를 활용하고자 한다. 이를 위해 그래머 퍼저를 사용한 페이로드를 생성 방법론을 제시하였고, 그래머 퍼징을 적용한 웹 취약점 스캐너인 web_fuzzer를 개발했다. 추가적으로 효과적인 웹 취약점 탐지를 위해 크롤링, 비동기, 병렬 처리의 중요성을 강조했다.
This research aims at a new practical Intent fuzzing tool for detecting Intent vulnerabilities of Android apps causing the robustness problem. We proposed two new ideas. First, we designed an Intent specification language to describe the structure of Intent, which makes our Intent fuzz testing tool flexible. Second, we proposed an automatic tally method classifying unique failures. With the two ideas, we implemented an Intent fuzz testing tool called Hwacha, and evaluated it with 50 commercial Android apps. Our tool offers an arbitrary combination of automatic and manual Intent generators with executors such as ADB and JUnit due to the use of the Intent specification language. The automatic tally method excluded almost 80% of duplicate failures in our experiment, reducing efforts of testers very much in review of failures. The tool uncovered more than 400 unique failures including what is unknown so far. We also measured execution time for Intent fuzz testing, which has been rarely reported before. Our tool is practical because the whole procedure of fuzz testing is fully automatic and the tool is applicable to the large number of Android apps with no human intervention.
본 논문에서는 3GPP(3rd Generation Partnership Project)에서 정의한 SMS PDU (Protocol Data Unit) 포맷을 주어진 SMS 부호화 복호화 모듈에서 정확하게 구현했는지 검증하는 방법을 제안한다. 기존 SMS 관련 도구들은 SMS 게이트웨이를 통해 송수신하거나 또는 SMS PDU 해석을 목적으로 개발되어 3GPP에서 정의한 세부 SMS PDU 규격에 따라 정확히 구현했는지 테스트하는 용도로는 적합하지 않다. 본 논문에서 제안한 방법은 함수형 언어 Haskell로 작성된 QuickCheck 라이브러리를 활용해 3GPP에서 정의한 구조에 맞는 SMS PDU 테스트 데이터를 자동 생성하여 SMS 부호화 복호화 모듈을 테스트한다. C언어로 작성된 리눅스 모바일 플랫폼 SMS 모듈에 적용하여 이 모듈의 부호화 복호화 기능을 테스트한 결과 BCD 포맷 시간 정보를 잘못 해석하는 사례 등 중요한 오류들을 발견할 수 있었다. 제안한 방법은 3GPP에서 정의한 규격에 맞추어 SMS PDU를 생성하기 때문에 일반적인 SMS 모듈들에 모두 적용 가능한 장점을 지닌다. 본 논문에서 사용한 방법과 같이 QuickCheck 라이브러리를 통해 다른 네트워크 프로토콜 데이터 규격에 대한 부호화 복호화 검증에도 응용할 수 있을 것이다. This paper proposes a test method for compliance of SMS encoder and decoder modules with 3GPP (3rd Generation Partnership Project) specification on SMS PDU (Protocol Data Unit). The existing tools have focused on providing an SMS gateway and on helping to view and edit a single SMS PDU, which rarely help to resolve the compliance test problem. The proposed compliance test method is based on an automatic generation of SMS PDUs fully compliant with the 3GPP specification by using QuickCheck library written in Haskell. By applying the proposed method to a C-based SMS encoder and decoder in Linux Mobile platform, we have found out several critical bugs such as wrong interpretation of time stamps in BCD format. The automatic SMS PDU generator is reusable in that it only depends on the 3GPP SMS specification. The QuickCheck library is also applicable for testing other network protocol data encoders and decoders, as used in this paper.