Hosei University Repository
Not a member yet
22008 research outputs found
Sort by
A Formal Engineering Approach for Interweaving Functional and Security Requirements of RESTful Web APIs
Get PDFRESTful Web API adoption has become ubiquitous with the proliferation of REST APIs in almost all domains with modern web applications embracing the micro-service architecture. This vibrant and expanding adoption of APIs, has made an increasing amount of data to be funneled through systems which require proper access management to ensure that web assets are secured. A RESTful API provides data using the HTTP protocol over the network, interacting with databases and other services and must preserve its security properties. Currently, practitioners are facing two major challenges for developing high quality secure RESTful APIs. One, REST is not a protocol. Instead, it is a set of guidelines that define how web resources can be designed and accessed over HTTP endpoints. There are a set of guidelines which stipulate how related resources should be structured using hierarchical URIs as well as how specific well-defined actions on those resources should be represented using different HTTP verbs. Whereas security has always been critical in the design of RESTful APIs, there are no clear formal models utilizing a secure-by-design approach that interweaves both the functional and security requirements. The other challenge is how to effectively utilize a model driven approach for constructing precise requirements and design specifications so that the security of a RESTFul API is considered as a concern that transcends across functionality rather than individual isolated operations.This thesis proposes a novel technique that encourages a model driven approach to specifying and verifying APIs functional and security requirements with the practical formal method SOFL (Structured-Object-Oriented Formal Language). Our proposed approach provides a generic 6 step model driven approach for designing security aware APIs by utilizing concepts of domain models, domain primitives, Ecore metamodel and SOFL. The first step involves generating a flat file with APIs resource listings. In this step, we extract resource definitions from an input RESTful API documentation written in RAML using an existing RAML parser. The output of this step is a flat file representing API resources as defined in the RAML input file. This step is fully automated. The second step involves automatic construction of an API resource graph that will work as a blue print for creating the target API domain model. The input for this step is the flat file generated from step 1 and the output is a directed graph (digraph) of API resource. We leverage on an algorithm which we created that takes a list of lists of API resource nodes and the defined API root resource node as an input, and constructs a digraph highlighting all the API resources as an output. In step 3, we use the generated digraph as a guide to manually define the API’s initial domain model as the target output with an aggregate root corresponding to the root node of the input digraph and the rest of the nodes corresponding to domain model entities. In actual sense, the generated digraph in step 2 is a barebone representation of the target domain model, but what is missing in the domain model at this stage in the distinction between containment and reference relationship between entities. The resulting domain model describes the entire ecosystem of the modeled API in the form of Domain Driven Design Concepts of aggregates, aggregate root, entities, entity relationships, value objects and aggregate boundaries. The fourth step, which takes our newly defined domain model as input, involves a threat modeling process using Attack Defense Trees (ADTrees) to identify potential security vulnerabilities in our API domain model and their countermeasures. aCountermeasures that can enforce secure constructs on the attributes and behavior of their associated domain entities are modeled as domain primitives. Domain primitives are distilled versions of value objects with proper invariants. These invariants enforce security constraints on the behavior of their associated entities in our API domain model. The output of this step is a complete refined domain model with additional security invariants from the threat modeling process defined as domain primitives in the refined domain model. This fourth step achieves our first interweaving of functional and security requirements in an implicit manner. The fifth step involves creating an Ecore metamodel that describes the structure of our API domain model. In this step, we rely on the refined domain model as input and create an Ecore metamodel that our refined domain model corresponds to, as an output. Specifically, this step encompasses structural modeling of our target RESTful API. The structural model describes the possible resource types, their attributes, and relations as well as their interface and representations. The sixth and the final step involves behavioral modeling. The input for this step is an Ecore metamodel from step 5 and the output is formal security aware RESTful API specifications in SOFL language. Our goal here is to define RESTful API behaviors that consist of actions corresponding to their respective HTTP verbs i.e., GET, POST, PUT, DELETE and PATCH. For example, CreateAction creates a new resource, an UpdateAction provides the capability to change the value of attributes and ReturnAction allows for response definition including the Representation and all metadata. To achieve behavioral modelling, we transform our API methods into SOFL processes. We take advantage of the expressive nature of SOFL processes to define our modeled API behaviors. We achieve the interweaving of functional and security requirements by injecting boolean formulas in post condition of SOFL processes. To verify whether the interweaved functional and security requirements implement all expected functions correctly and satisfy the desired security constraints, we can optionally perform specification testing. Since implicit specifications do not indicate algorithms for implementation but are rather expressed with predicate expressions involving pre and post conditions for any given specification, we can substitute all the variables involved a process with concrete values of their types with results and evaluate their results in the form of truth values true or false. When conducting specification testing, we apply SOFL process animation technique to obtain the set of concrete values of output variables for each process functional scenario. We analyse test results by comparing the evaluation results with an analysis criteria. An analysis criteria is a predicate expression representing the properties to be verified. If the evaluation results are consistent with the predicate expression, the analysis show consistency between the process specification and its associated requirement. We generate the test cases for both input and output variables based on the user requirements. The test cases generated are usually based on test targets which are predicate expressions, such as the pre and post conditions of a process. when testing for conformance of a process specification to its associated service operation, we only need to observe the execution results of the process by providing concrete input values to all of its functional scenarios and analyze their defining conditions relative to user requirements. We present an empirical case study for validating the practicality and usability of our model driven formal engineering approach by applying it in developing a Salon Booking System. A total of 32 services covering functionalities provided by the Salon Booking System API were developed. We defined process specifications for the API services with their respective security requirements. The security requirements were injected in the threat modeling and behavioral modeling phase of our approach. We test for the interweaving of functional and security requirements in the specifications generated by our approach by conducting tests relative to original RAML specifications. Failed tests were exhibited in cases where injected security measure like requirement of an object level access control is not respected i.e., object level access control is not checked. Our generated SOFL specification correctly rejects such case by returning an appropriate error message while the original RAML specification incorrectly dictates to accept such request, because it is not aware of such measure. We further demonstrate a technique for generating SOFL specifications from a domain model via model to text transformation. The model to text transformation technique semi-automates the generation of SOFL formal specification in step 6 of our proposed approach. The technique allows for isolation of dynamic and static sections of the generated specifications. This enables our technique to have the capability of preserving the static sections of the target specifications while updating the dynamic sections in response to the changes of the underlying domain model representing the RESTful API in design. Specifically, our contribution is provision of a systemic model driven formal engineering approach for design and development of secure RESTful web APIs. The proposed approach offers a six-step methodology covering both structural and behavioral modelling of APIs with a focus on security. The most distinguished merit of the model to text transformation is the utilization of the API’s domain model as well as a metamodel that the domain model corresponds to as the foundation for generation of formal SOFL specifications that is a representation of API’s functional and security requirements.博士(理学)法政大学 (Hosei University
«La singularité de Staline : réflexions à propos de l’étude sur l’U.R.S.S. dans le Tome II de la Critique de la raison dialectique de Sartre»
Get PDFExplikation der Vorrede der Phänomenologie des Geistes Hegels （die Absätze 71-72）
Get PDFDie Absätze 71-72 machen den Schluss der Vorrede der Phänomenologie des Geistes Hegels aus. Erstens wurde die spekulative Philosophie das gegenwärtige Publikum durchdringen, wenn die gegenwärtige Zeit die des Neuplatonismus wäre. Zweitens wird die spekulative Philosophie die Allgemeinheit des Geistes langsam und still durchdringen. Denn die Allgemeinheit des Geistes bedarf die Ankunft der Zeit
Feature Articles “Japanese Studies and Transnationalism” (The 4th EU-Japan Young Scholars Workshop /2021 International New Generation Workshop) : Transnationalism in Literature and Its Reception : a Case Study of Zainichi Literature
Get PDFThe Zainichi writers sought during the 1960s and the 1970s to question the notion of national literature, one that would be rooted in the idea of a monolingual and mono-ethnic Nation State. In this sense, we can consider their approach transnational. The number of their publications grew steadily in Japan from the 1960s onwards, and consequently, at this point, the literary world was forced to recognize and include them as a category. While this opened the way for writers to gain public acknowledgement through literary prizes, it also required them to be an integral part of Japanese literature and to conform to its aesthetic standards. Some of the themes - the issue of split identity or the transnational journey of Zainichi family - as well as the language they used to express the bilingual or bicultural world sometimes met with rejection from Japanese critics and writers. To what extent can language-dependent literature be transnational? What possibility do writers have to express transnationality all the while having no other choice but to aim at the national literary terrain in order to get published? This article attempts to answer these questions by using the example of Zainichi literature and by analyzing the reactions it provoked in the Japanese literary world at the time
Accuracy Assessment and Improvement of FMCW Radar-based Vital Signs Monitoring under Practical Scenarios
Get PDFAcquisition of human vital signs through radar is a very promising technology that can address the shortcomings of the traditional contact-based measurement devices and enable the move toward a contactless vital monitoring system. This research is focused on monitoring breath rate (BR) and heart rate (HR) via a frequency modulated continuous wave (FMCW) radar. Currently, the two approaches used for BR and HR estimation are filter-based and decomposition-based, such as variational mode decomposition (VMD) for high-quality signal separation. We propose an adaptive VMD (AVMD) to address the problem of setting the number of segmentation levels required by the VMD algorithm. Various experiments are conducted under practical scenarios in terms of distance, angle, posture, and activity as well as the existence of a nearby person and fan. We have made a comprehensive assessment of accuracy change and impact in these scenarios. The experimental results show clearly that the proposed AVMD gives higher accuracy compared to the filter-based and VMD-based. A real-time BR-HR monitoring system using the proposed AVMD and the TI’s IWR1843Boost radar board has been implemented to demonstrate its practical uses
Cross-Lingual Transfer Learning Approach to Pronunciation Error Detection via Latent Phonetic Representation
Get PDFExtensive research has been conducted on CALL systems for Pronunciation Error detection to automate language improvement through self-evaluation. However, many of these previous approaches have relied on HMM or Neural Network Hybrid Models which, although have proven to be effective, often utilize phonetically labelled L2 speech data which is expensive and often scarce. This paper discusses a ”zero-shot” transfer learning approach to detect phonetic errors in L2 English speech by Japanese native speakers using solely unaligned phonetically labelled native Language speech. The proposed method introduces a simple base architecture which utilizes the XLSR-Wav2Vec2.0 model pre-trained on unlabelled multilingual speech. Phoneme mapping for each language is determined based on difference of articulation of similar phonemes. This method achieved a Phonetic Error Rate of 0.214 on erroneous L2 speech after fine-tuning on 70 hours of speech with low resource automated phonetic labelling, and proved to additionally model phonemes of the native language of the L2 speaker effectively without the need for L2 speech fine-tuning
Hybrid interconnection topologies for high performance and low hardware cost based on hypercube and k-ary n-tree
Get PDFThe implementation of fat-tree interconnection networks is prevalent in high-performance parallel computing. However, the traditional fat-tree structure requires a considerable amount of switches and links to connect computing nodes, resulting in a significant increase in hardware costs for large-scale high-performance systems. This study proposes two innovative hybrid topologies, the k-ary n-tree k-cube (KANTC) and the Mirrored k-ary n-tree k-cube (MiKANTC), to address the aforementioned issue. The proposed topologies merge the characteristics of the hypercube and fat-tree structures. Instead of the traditional direct connection of k computing nodes to an edge-level switch, the edge-level switches in the fat-tree are substituted with k-cubes. This results in the formation of k^n−2 k-cubes at the edge level, where each k-cube links k switches to the upper level of the k-ary n-tree, while the remaining switches link to the compute nodes. Hence, all the cubes are capable of interconnecting k(2^k−k) compute nodes. Shortest path-based routing algorithms are proposed for these hybrid topologies, and several link fault tolerant routing algorithms are developed to enhance the fault tolerance of the entire topology. The proposed hybrid topologies are then evaluated in terms of path diversity, cost, and performance. The results demonstrates that the proposed KANTC and MiKANTC topologies exhibit improved performance, with up to 84% reduction in the number of switches and 78% reduction in links in large parallel systems when k = n = 8, compared to the conventional fat-tree topology. Additionally, these hybrid topologies display enhanced path diversity compared to traditional fat-tree