Search

Detecting programming errors and vulnerabilities in software is increasingly important, and building tools that help with this task is an area of investigation, crucial for the industry these days. When programming in an object-oriented language, one naturally defines stateful objects that are non-uniform, i.e., their methods’ availability depends on their internal state. One might represent their intended usage protocol with an automaton or a state machine. Behavioral types allow to statically check if all the code of a program respects the usage protocol of each object. In this thesis we present a tool that extends Java with typestate definitions. These typestates are associated with Java classes and define the behavior of instances of those classes, specifying the sequences of method calls allowed. This tool checks statically that method calls happen in order, following the specified behavior. The tool was implemented in Kotlin as a plugin for the Checker Framework. It is a new implementation of the Mungo tool and supports prevention of null pointer errors, state transitions depending on return values, assurance of protocol completion, droppable states, and association of protocols with classes from the standard Java library or from third-party libraries. Additionally, the tool integrates behavioral types with access permissions, allowing objects to be shared in a controlled way using a language of assertions. This language of assertions supports concepts like packing and unpacking, including unpacking of aliases objects, and transferring of permissions between aliases. To relieve the programmer from manually writing all the necessary assertions, the tool implements an inference algorithm which analyzes the code statically and, given the uses of objects, constructs all the required assertions. A deteção de erros de programação e vulnerabilidades no software é cada vez mais importante, e a criação de ferramentas que ajudem nesta tarefa é uma área de investigação crucial para a indústria atualmente. Ao programar numa linguagem orientada a objetos, definem-se naturalmente objetos com estado que não são uniformes, ou seja, a disponibilidade dos seus métodos depende do seu estado interno. Pode-se representar o protocolo de uso pretendido com um autómato ou uma máquina de estados. Os tipos comportamentais permitem verificar estaticamente se todo o código de um programa respeita o protocolo de uso de cada objeto. Nesta tese apresentamos uma ferramenta que estende o Java com definições de typestates. Esses estão associados às classes Java e definem o comportamento das instâncias dessas classes, especificando as sequências de chamadas de métodos permitidas. Esta ferramenta verifica estaticamente se as chamadas de métodos ocorrem pela ordem correta, seguindo o comportamento especificado. A ferramenta foi implementada em Kotlin como um plugin para o Checker Framework. É uma implementação nova da ferramenta Mungo e suporta a prevenção de erros de ponteiro nulo, transições de estado dependendo de valores de retorno, asseguração da conclusão dos protocolos, objetos que podem ser «largados», e a associação de protocolos com classes da biblioteca padrão do Java ou de terceiros. Além disso, esta integra tipos comportamentais com permissões de acesso, permitindo que objetos possam ser partilhados por meio de uma linguagem de asserções. Esta linguagem de asserções oferece suporte para conceitos como packing e unpacking, incluindo unpacking de objetos partilhados, e transferência de permissões entre variáveis que apontam para o mesmo objeto. Para aliviar o programador de escrever manualmente todas as asserções necessárias, a ferramenta implementa um algoritmo de inferência que analisa o código estaticamente e, consoante os usos dos objetos, constrói todas as asserções necessárias.

Part 2: Communications: Types and Implemenations; International audience; Detecting programming errors and vulnerabilities in software is increasingly important, and building tools that help developers with this task is a crucial area of investigation on which the industry depends. In object-oriented languages, one naturally defines stateful objects where the safe use of methods depends on their internal state; the correct use of objects according to their protocols is then enforced at compile-time by an analysis based on behavioral types.We present Java Typestate Checker (JATYC), a tool based on the Checker Framework that verifies Java programs with respect to typestates. These define the object’s states, the methods that can be called in each state, and the states resulting from the calls. The tool offers the following strong guarantees: sequences of method calls obey to object’s protocols; completion of objects’ protocols; detection of null-pointer exceptions; and control of the sharing of resources through access permissions.To the best of our knowledge, there are no research or industrial tools that offer all these features. In particular, the implementation of sharing control in a typestate-based tool seems to be novel, and has an important impact on programming flexibility, since, for most programs, the linear discipline imposed by behavioral types is too strict.Sharing of objects is enabled by means of an assertion language incorporating fractional permissions; to lift from programmers the burden of writing the assertions, JATYC infers all of these by building a constraint system and solving it with Z3, producing general assertions sufficient to accept the code, if these exist.

Informacijos ir informacinių technologijų apsauga – tai įrankių ir sprendimų visuma, taikoma siekiant apsaugoti tai, kas dabar svarbiausia – informaciją. Dėl įvairių išorinių ir vidinių veiksnių nuolat kyla grėsmė šiam turtui būti tyčia ar netyčia pažeistam, pakeistam ar sunaikintam. Apsauga neapsiriboja vien tik fiziniu pačios įrangos saugumu, dabar plačiai taikomos papildomos programinės priemonės, kurios didiną saugumą ir kontrolę, ir tik kompleksiškas ir apgalvotas tokių priemonių naudojimas užtikrina informacijos vientisumą, prieinamumą ir konfidencialumą. Be gausybės technologinių sprendimų, rinkoje siūlomi gerųjų informacinės saugos praktikų rinkiniai, kurių tinkamas pritaikymas organizacijose yra net svarbesnis nei skirtingų apsaugos mechanizmų ar taikomųjų programų duodama nauda. Dauguma šios srities specialistų sutaria, kad gerai įgyvendinta informacinės saugos politika yra kritiškai svarbus visapusiškos saugos elementas. Deja, ne kiekviena įmonė pasiruošusi tokios politikos pritaikymui dėl įvairių priežasčių – nepakankamas noras keistis, atsisakyti ydingų įpročių ir praktikų, verslo modelio nesuderinamumas su bandoma pritaikyti politika, tinkamų specialistų trūkumas ir pan., o kur dar priežiūra ir palaikymas po politikos įgyvendinimo, auditas, ar viskas atlikta tinkamai ir taip, kaip politika reikalavo. Todėl svarbu iškilusius iššūkius spręsti, bandant panaudoti automatizavimo galimybes, kas palengvintų administratorių ir organizacijos vadovų darbą, sąnaudas bei visą tai leistų nukreipti į kitas silpnesnes saugos sritis. Prieigos saugos politika yra bene pagrindinė politika iš viso rinkinio ir jos įgyvendinimas duoda didžiausią naudą, todėl kaip įmanoma supaprastinus ir automatizavus jos pritaikymą, būtų galima visoms organizacijoms pasiūlyti ją susidiegti ir taip paskatinti pradėti rūpintis savo informacinių šaltinių apsaugą., Security of information and information technologies – that’s a collection of tools and solutions to reach the highest possible security level to protect the most valuable resource – information. Because of many different external and internal factors there is constant threat for this asset to be modified, leaked or deleted. The security is never only physical perimeter protection, it is a combination of physical and cyber security, and only this kind of approach could help organization stick to CIA model. Despite all the security software and hardware out there in the market, there are also sets of best practices which provide great value if implemented properly. Many IT security professionals agree that well implemented information security policy is crucial for any organization. Unfortunately, not everyone is prepared to handle this kind of task because of its complexity, confrontation with business model, lack of specialists and so on. Moreover, it has to be well maintained and audited, so it is important to solve similar issues by using automation where possible. That could save effort and money for business. Access security policy is fundamental for all the security policy, so it would give a great value if organization could implement at least that one. So automatization of the process would let many other organizations have this implementation finally available and that could be a great start to take care of information security.