19 research outputs found
الشيخ السيّد نفيس الحسيني رحمة اللہ علیہ حیاتہ و آثارہ: SAYYED NAFEES Al-HUSSAINI: LIFE AND WORK
No full textSayyed Nafees Al-Hussaini, may God have mercy on him, was of high lineage, a great Sufi, a talented poet, a great author, and a professor. His full name was Sayyed Anwar Hussain S/O Sayyed Muhammad Ashraf Ali. Sayyed Nafees Al-Husseini was born on Saturday 13 Dhul-Qi’dah in the year 1351 AH, corresponding to March 11, 1933 AD, in the village of Kahoriala in the Sialkot District. He did not study in Arab Islamic religious schools and was not a graduate of Islamic universities, but God Almighty gave him knowledge, extensive information from Himself, and insight. Sayyed Nafees says that he moved from Faisalabad to Lahore in the month of Zul-Hajj in the year 1370 AH/September 1951 AD. Here, after a short time, I met the writer and calligrapher Taj al-Din, known as Zarrin. Sayyed Nafees used to teach people the art of calligraphy and teach students who longed to teach writing and the art of calligraphy. Sayyed Nafees was a talented poet, and his passion for poetry was innate to him. He started reciting poetry when he was a high school student. He wrote poetry by calling him “Zaidi” and “Nafees.” The subject of his poetry was love for the Prophet, may God bless him and grant him peace, and love for his family and companions. He published collections of his poetry, “Nafa’is al-Nabi(SAAW)” and “Barg e Gul”. Sayyed Nafees Al-Hussaini died on February 5, 2008 AD. Abd al-Rashid Qamar says about him: “There is no doubt that Sayyed Nafees al-Hussaini was elected by God. Divine power opened the door to spirituality before him during his writing. According to people of thought and theory, Sayyed was a religious leader.” I hope this article may help the readers to enhance knowledge about the great Sufi, a talented poet and a great author
Analysis and Composition of Multiple Aspects in Aspect Oriented Programs
No full textInternational audienceThis paper presents a classification of widely studied approaches that focus interaction analysis and composition of multiple aspect(s) in aspect-oriented programs (AOP). It is evident that AOP has an ability to distort semantics of base-programs and aspects themselves due to advice-method or advice-advice interactions in terms of control flow and data sharing features. Thus, it entails a comprehensive analysis in order to pinpoint ambiguities at semantic level; especially in case of multiple aspects that remains focus of this paper. One possible interaction (method-advice) may inviolate a predicate of another advice from another aspect, residing in the base-program. We narrow our analysis to understand such intricacies and present a bunch of rules to understand weaving semantics (in particular, advice-advice interaction from two different aspects) and also propose precedence laws for aspects to be woven. In this paper discrete computation of aspects using operational semantics enables better interaction analysis of aspects and specifying their behavior by excluding the dependencies of any specific AOP language implementation. The contributions are threefold: (1) a survey based on an informal classification of proposed approaches targeted towards interfering aspects (2) our proposed formal definitions for composing aspects through evaluation rules using operational semantics (3) addressing precedence issues in aspects to some degree and offering a preliminary solution based on proactive execution order of aspects
Spécification et animation de modèles de conception de la sécurité avec Z
No full textSpecifying security-critical software urges to develop techniques that allow early bugs detection and prevention. This is aggravated by the fact that massive cost and time are spent during product validation and verification (V&V). There exists a multitude of formal and informal techniques striving to confront the challenge of specifying and validating specifications. Our approach mainly concerns validating the security specifications by animating the formal models, which adds a new dimension to the state-of-the-art.Secure system engineering dedicated to tackle security features offers security-design models to sketch secure applications. Generally for these, Unified Modeling Language (UML) is considered a de facto standard along with a few extensions such as SecureUML and Object Constraint Language (OCL). OCL tends to add precision in design but yet it remains far from obtaining bugs free specifications. One reason to that is the inability of the OCL-based techniques to animate models before proceeding to an implementation.Combining formal languages such as Z with UML allows applying animation techniques enabling early validation of software design. The RoZ tool is capable of translating UML models into the Z specifications which further can be verified or validated. But RoZ is lacking to provide similar features for secure applications. In this thesis, we have upgraded this tool using an underlying security kernel backed up by Role Based Access Control (RBAC). Our approach not only allows validating the specifications but can animate the formal models. The animation also takes into account both the static and the dynamic aspects (i.e., session management) of RBAC-based security policies. Our unified approach and toolset involves a systematic usage and linkage of UML, SecureUML, RBAC, RoZ, Z, and the Just Another Z Animator (Jaza) tool. Using Jaza, the sort of validation we perform allows enumerating user defined scenarios to determine if the specification describes the intended reality. We emphasize on simultaneous consideration of functional and non-functional properties and consider functional models as contextual constraints over the security models. From a user viewpoint, our proposed approach can arbitrarily be composed with any functional model to examine an RBAC-based security policy.L'écriture de spécifications pour des logiciels en général et en particulier pour des applications sécurisées demande de développer des techniques qui facilitent la détection et la prévention des erreurs de conception, dès les premières phases du développement. Ce besoin est motivé par les coûts et délais des phases de vérification et validation. De nombreuses méthodes de spécification, tant formelles qu'informelles ont été proposées et, comme nous le verrons dans cette thèse, les approches formelles donnent des spécifications de meilleure qualité.L'ingénierie des systèmes sécurisés propose l'utilisation de modèles de conception de la sécurité pour représenter les applications sécurisées. Dans de nombreux cas, ces modèles se basent sur les notations graphiques d'UML avec des extensions, sous forme de profils comme SecureUML, pour exprimer la sécurité. Néanmoins, les notations d'UML, même étendues avec des assertions OCL, sont insuffisantes pour garantir la correction de ces modèles. Ceci est notamment du aux limites des outils d'animation utilisés pour valider des modèles UML étendus en OCL. Nous proposons de combiner des langages formels comme Z avec UML pour valider des applications en animant leurs spécifications, indépendamment de futurs choix d'implémentation. Le but de cette thèse est de présenter une approche pour analyser par animation des modèles de conception de la sécurité. Nous utilisons un outil pré-existant, RoZ, pour traduire les aspects fonctionnels du modèle UML en Z. Cependant, RoZ ne couvre pas la modélisation des aspects sécuritaires. Dans cette thèse, nous avons complété l'outil RoZ en l'associant à un noyau de sécurité qui spécifie les concepts du modèle RBAC (Role Based Access Control). Nous utilisons l'animation pour explorer dynamiquement et ainsi valider les aspects sécuritaires de l'application.Notre approche et les outils qui la supportent intègrent UML, SecureUML (un langage de modélisation de la sécurité), RBAC, RoZ, Z et Jaza, un animateur pour le langage Z. L'animation des spécifications prend la forme de scénarios définis par l'utilisateur qui permettent de se convaincre que la spécification décrit correctement ses besoins. Notre approche permet une validation dès la phase de spécification, qui prend en considération l'interaction entre les modèles fonctionnel et sécuritaire, et qui fait abstraction des choix de l'implémentation. Les éléments du modèle fonctionnel peuvent être utilisés comme contexte dans la définition des permissions du modèle de sécurité. Notre approche ne met pas de contrainte sur ce modèle fonctionnel ce qui permet de l'utiliser pour une vaste gamme d'applications
Specification and animation of security design models using Z
No full textL'écriture de spécifications pour des logiciels en général et en particulier pour des applications sécurisées demande de développer des techniques qui facilitent la détection et la prévention des erreurs de conception, dès les premières phases du développement. Ce besoin est motivé par les coûts et délais des phases de vérification et validation. De nombreuses méthodes de spécification, tant formelles qu'informelles ont été proposées et, comme nous le verrons dans cette thèse, les approches formelles donnent des spécifications de meilleure qualité.L'ingénierie des systèmes sécurisés propose l'utilisation de modèles de conception de la sécurité pour représenter les applications sécurisées. Dans de nombreux cas, ces modèles se basent sur les notations graphiques d'UML avec des extensions, sous forme de profils comme SecureUML, pour exprimer la sécurité. Néanmoins, les notations d'UML, même étendues avec des assertions OCL, sont insuffisantes pour garantir la correction de ces modèles. Ceci est notamment du aux limites des outils d'animation utilisés pour valider des modèles UML étendus en OCL. Nous proposons de combiner des langages formels comme Z avec UML pour valider des applications en animant leurs spécifications, indépendamment de futurs choix d'implémentation. Le but de cette thèse est de présenter une approche pour analyser par animation des modèles de conception de la sécurité. Nous utilisons un outil pré-existant, RoZ, pour traduire les aspects fonctionnels du modèle UML en Z. Cependant, RoZ ne couvre pas la modélisation des aspects sécuritaires. Dans cette thèse, nous avons complété l'outil RoZ en l'associant à un noyau de sécurité qui spécifie les concepts du modèle RBAC (Role Based Access Control). Nous utilisons l'animation pour explorer dynamiquement et ainsi valider les aspects sécuritaires de l'application.Notre approche et les outils qui la supportent intègrent UML, SecureUML (un langage de modélisation de la sécurité), RBAC, RoZ, Z et Jaza, un animateur pour le langage Z. L'animation des spécifications prend la forme de scénarios définis par l'utilisateur qui permettent de se convaincre que la spécification décrit correctement ses besoins. Notre approche permet une validation dès la phase de spécification, qui prend en considération l'interaction entre les modèles fonctionnel et sécuritaire, et qui fait abstraction des choix de l'implémentation. Les éléments du modèle fonctionnel peuvent être utilisés comme contexte dans la définition des permissions du modèle de sécurité. Notre approche ne met pas de contrainte sur ce modèle fonctionnel ce qui permet de l'utiliser pour une vaste gamme d'applications.Specifying security-critical software urges to develop techniques that allow early bugs detection and prevention. This is aggravated by the fact that massive cost and time are spent during product validation and verification (V&V). There exists a multitude of formal and informal techniques striving to confront the challenge of specifying and validating specifications. Our approach mainly concerns validating the security specifications by animating the formal models, which adds a new dimension to the state-of-the-art.Secure system engineering dedicated to tackle security features offers security-design models to sketch secure applications. Generally for these, Unified Modeling Language (UML) is considered a de facto standard along with a few extensions such as SecureUML and Object Constraint Language (OCL). OCL tends to add precision in design but yet it remains far from obtaining bugs free specifications. One reason to that is the inability of the OCL-based techniques to animate models before proceeding to an implementation.Combining formal languages such as Z with UML allows applying animation techniques enabling early validation of software design. The RoZ tool is capable of translating UML models into the Z specifications which further can be verified or validated. But RoZ is lacking to provide similar features for secure applications. In this thesis, we have upgraded this tool using an underlying security kernel backed up by Role Based Access Control (RBAC). Our approach not only allows validating the specifications but can animate the formal models. The animation also takes into account both the static and the dynamic aspects (i.e., session management) of RBAC-based security policies. Our unified approach and toolset involves a systematic usage and linkage of UML, SecureUML, RBAC, RoZ, Z, and the Just Another Z Animator (Jaza) tool. Using Jaza, the sort of validation we perform allows enumerating user defined scenarios to determine if the specification describes the intended reality. We emphasize on simultaneous consideration of functional and non-functional properties and consider functional models as contextual constraints over the security models. From a user viewpoint, our proposed approach can arbitrarily be composed with any functional model to examine an RBAC-based security policy
Spécification et animation de modèles de conception de la sécurité avec Z
No full textL'écriture de spécifications pour des logiciels en général et en particulier pour des applications sécurisées demande de développer des techniques qui facilitent la détection et la prévention des erreurs de conception, dès les premières phases du développement. Ce besoin est motivé par les coûts et délais des phases de vérification et validation. De nombreuses méthodes de spécification, tant formelles qu'informelles ont été proposées et, comme nous le verrons dans cette thèse, les approches formelles donnent des spécifications de meilleure qualité.L'ingénierie des systèmes sécurisés propose l'utilisation de modèles de conception de la sécurité pour représenter les applications sécurisées. Dans de nombreux cas, ces modèles se basent sur les notations graphiques d'UML avec des extensions, sous forme de profils comme SecureUML, pour exprimer la sécurité. Néanmoins, les notations d'UML, même étendues avec des assertions OCL, sont insuffisantes pour garantir la correction de ces modèles. Ceci est notamment du aux limites des outils d'animation utilisés pour valider des modèles UML étendus en OCL. Nous proposons de combiner des langages formels comme Z avec UML pour valider des applications en animant leurs spécifications, indépendamment de futurs choix d'implémentation. Le but de cette thèse est de présenter une approche pour analyser par animation des modèles de conception de la sécurité. Nous utilisons un outil pré-existant, RoZ, pour traduire les aspects fonctionnels du modèle UML en Z. Cependant, RoZ ne couvre pas la modélisation des aspects sécuritaires. Dans cette thèse, nous avons complété l'outil RoZ en l'associant à un noyau de sécurité qui spécifie les concepts du modèle RBAC (Role Based Access Control). Nous utilisons l'animation pour explorer dynamiquement et ainsi valider les aspects sécuritaires de l'application.Notre approche et les outils qui la supportent intègrent UML, SecureUML (un langage de modélisation de la sécurité), RBAC, RoZ, Z et Jaza, un animateur pour le langage Z. L'animation des spécifications prend la forme de scénarios définis par l'utilisateur qui permettent de se convaincre que la spécification décrit correctement ses besoins. Notre approche permet une validation dès la phase de spécification, qui prend en considération l'interaction entre les modèles fonctionnel et sécuritaire, et qui fait abstraction des choix de l'implémentation. Les éléments du modèle fonctionnel peuvent être utilisés comme contexte dans la définition des permissions du modèle de sécurité. Notre approche ne met pas de contrainte sur ce modèle fonctionnel ce qui permet de l'utiliser pour une vaste gamme d'applications.Specifying security-critical software urges to develop techniques that allow early bugs detection and prevention. This is aggravated by the fact that massive cost and time are spent during product validation and verification (V&V). There exists a multitude of formal and informal techniques striving to confront the challenge of specifying and validating specifications. Our approach mainly concerns validating the security specifications by animating the formal models, which adds a new dimension to the state-of-the-art.Secure system engineering dedicated to tackle security features offers security-design models to sketch secure applications. Generally for these, Unified Modeling Language (UML) is considered a de facto standard along with a few extensions such as SecureUML and Object Constraint Language (OCL). OCL tends to add precision in design but yet it remains far from obtaining bugs free specifications. One reason to that is the inability of the OCL-based techniques to animate models before proceeding to an implementation.Combining formal languages such as Z with UML allows applying animation techniques enabling early validation of software design. The RoZ tool is capable of translating UML models into the Z specifications which further can be verified or validated. But RoZ is lacking to provide similar features for secure applications. In this thesis, we have upgraded this tool using an underlying security kernel backed up by Role Based Access Control (RBAC). Our approach not only allows validating the specifications but can animate the formal models. The animation also takes into account both the static and the dynamic aspects (i.e., session management) of RBAC-based security policies. Our unified approach and toolset involves a systematic usage and linkage of UML, SecureUML, RBAC, RoZ, Z, and the Just Another Z Animator (Jaza) tool. Using Jaza, the sort of validation we perform allows enumerating user defined scenarios to determine if the specification describes the intended reality. We emphasize on simultaneous consideration of functional and non-functional properties and consider functional models as contextual constraints over the security models. From a user viewpoint, our proposed approach can arbitrarily be composed with any functional model to examine an RBAC-based security policy.SAVOIE-SCD - Bib.électronique (730659901) / SudocGRENOBLE1/INP-Bib.électronique (384210012) / SudocGRENOBLE2/3-Bib.électronique (384219901) / SudocSudocFranceF
Assessing farmers’ perspectives on climate change for effective farm-level adaptation measures in Khyber Pakhtunkhwa, Pakistan
No full textAgriculture is considered as the backbone of the economy of Pakistan. However, current changes in climate have been adversely affecting agricultural productivity. In this paper, perceived impacts of climate change on agriculture and adaptation towards it have been studied in Charsadda district (lowlands) of Khyber Pakhtunkhwa province of Pakistan through extensive field surveys, involving 116 farm households. Results have revealed that climate change factors including fluctuating temperature, evidence of yearly long droughts, and a steady shift in rainfall patterns have pressured the agriculture sector and livelihoods of the local peasants. The staggering floods of 2010 and 2011 in Pakistan have evidenced severe climatic changes in Pakistan. These countrywide floods have washed fertile soil in the study area that has directly contributed to losses in agricultural yield and increased vector-borne diseases in crops. The local farmers have commonly deployed adaptive measure such as crops diversification, changing fertilizer, and planting shaded trees to minimize the impacts of changes in climate. However, these adjustments measures are perceived as not appropriate for improving farm yield. Therefore, the study suggests that improved understanding of the climate change impacts and knowledge on adapting adequately will lead to no-regret adaptation. It will also help protecting farmer's lives and livelihoods and will boost their resilience towards changing climatic conditions
Evaluating RBAC Supported Techniques and their Validation and Verification
No full textInternational audienceThis paper evaluates the security specification techniques that employ Role Based Access Control (RBAC) variants. RBAC offers a special kind of access control mechanism based on the use of roles to grant permissions. Its variants include role hierarchy and separation of duty (SoD) constraints. The overall management of a RBAC supported system is made through its administrative, review and supporting system functions. In this paper, a summary of semi-formal and formal techniques employing RBAC is provided along with their benefits and limitations. Here, semi-formal techniques refer to UML+OCL while formal ones are based on Alloy. This paper may guide through the process of selecting an appropriate technique to specify security rules. This is done by analyzing the degree of coverage of RBAC including some extensions like SoD and role hierarchy. We also investigate the use of validation and verification tools in these techniques. We find that formal techniques are more amenable to automated analysis as compared to semi-formal ones. Semi-formal techniques are rich in specifying RBAC variants but have prototypic tools. Session based dynamic aspects of RBAC have been partly covered in both techniques
Validation of Security-Design Models using Z
No full textInternational audienceThis paper is aimed at formally specifying and validating security-design models of an information system. It combines graphical languages and formal methods, integrating specification languages such as UML and an extension, SecureUML, with the Z language. The modeled system addresses both functional and security requirements of a given application. The formal functional specification is built automatically from the UML diagram, using our RoZ tool. The secure part of the model instanciates a generic security-kernel written in Z, free from applications specificity, which models the concepts of RBAC (Role-Based Access Control). The final modeling step creates a link between the functional model and the instanciated security kernel. Validation is performed by animating the model, using the Jaza tool. Our approach is demonstrated on a case-study from the health care sector where confidentiality and integrity appear as core challenges to protect medical records
An Automatable Framework for Formal Specification & Verification of Aspect Oriented Programs
No full textAbstract. Formal verification of software is a perennial problem and an inclusion to formal verification challenges is AOP (Aspect Oriented programs). Likewise, several contrary formal verification approaches exist for OOP (Object Oriented programs) but unable to deliver same robustness for AOP verification and also the proposed approaches to verify AOP seem to be less effective because of their adoptability for large systems. Although we believe that the potential solution would be to choose best existing formal methods for formal verification of AOP to avoid unnecessary additions and modifications in current state of the art. This paper gives a thorough survey of the existing work. The paper presents a holistic framework for formal verification of AOP by formally specifying aspects and classes, autonomously. Then the obtained specifications are integrated to get filtered definition of the AOP, i.e., merging the aspect specification with the class specification to preserve execution order of an AO program. Besides, to verify augmented system, the derivation of classes through de-compilation from compiled AOP is attained for generating their corresponding formal specifications. Former and latter generated formal specifications are compared to analyze the intended and exotic behavior of aspects. This helps us to ensure that the actual behavior of the system is according to the one specified. Additionally, our approach helps to identify ambiguities and contradictions present in the compiled AOP, and allows to eliminate them. We use Object-Z to write classes and propose our own notations and constructs for describing aspects and for formulating filtered formal specification of classes and aspects using the notion of filters from RTOZ (Real Time Object-Z ∗). A possible tool support realizes the automation process of the framework. *is a senior member of Center for Software Dependability and presently working a
LUCRATIVENESS OF ISLAMIC VS CONVENTIONAL MUTUAL FUNDS IN PAKISTAN
No full textThe purpose of this study is to conduct a comparative riskadjusted performance, selectivity skills and market timing abilitiesanalysis of Islamic and Conventional mutual funds in Pakistan. Thestudy utilizes various risk-adjusted performance measures to evaluaterisk and return characteristics. The study also used techniqueproposed by (Treynor and Mazuy 1966) and (Henriksson and Merton1981) to appraise selectivity skills and timing abilities on the dataset ranging 2009-2013 of Islamic and Conventional mutual funds. Inthis study, four categories Aggressive Fixed Income, Asset Allocation,Equity and Balanced open end mutual funds are analysed. On thebasis of evidences found, only few mutual fund managers from Islamicand Conventional mutual funds hold better stock picking skills. Themutual fund managers of both Islamic and conventional mutual fundsare found to be a poor market timer in Pakistan. Islamic mutualfunds have earned better returns than conventional mutual funds.Therefore, risk adjusted performance of Islamic mutual funds is betterthan conventional mutual funds
